### Nuprl Lemma : weak-antecedent-surjection_functionality_wrt_pred_equiv

`∀es:EO`
`  ∀[P1,P2,Q1,Q2:E ─→ ℙ].  ∀f:{e:E| P1 e}  ─→ {e:E| Q1 e} . (P1 `⇐⇒` P2 `` Q1 `⇐⇒` Q2 `` (Q1 ←←= f== P1 `⇐⇒` Q2 ←←= f== P2))`

Proof

Definitions occuring in Statement :  weak-antecedent-surjection: `Q ←←= f== P` es-E: `E` event_ordering: `EO` predicate_equivalent: `P1 `⇐⇒` P2` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ─→ B[x]`
Lemmas :  subtype_rel_sets equal_wf set_wf weak-antecedent-surjection_wf subtype_rel_dep_function es-E_wf all_wf iff_wf event_ordering_wf
\mforall{}es:EO
\mforall{}[P1,P2,Q1,Q2:E  {}\mrightarrow{}  \mBbbP{}].
\mforall{}f:\{e:E|  P1  e\}    {}\mrightarrow{}  \{e:E|  Q1  e\}  .  (P1  \mLeftarrow{}{}\mRightarrow{}  P2  {}\mRightarrow{}  Q1  \mLeftarrow{}{}\mRightarrow{}  Q2  {}\mRightarrow{}  (Q1  \mleftarrow{}\mleftarrow{}=  f==  P1  \mLeftarrow{}{}\mRightarrow{}  Q2  \mleftarrow{}\mleftarrow{}=  f==  P2))

Date html generated: 2015_07_17-AM-09_02_28
Last ObjectModification: 2015_01_27-PM-00_55_44

Home Index