### Nuprl Lemma : weak-antecedent-surjections-compose

`∀es:EO`
`  ∀[P,Q,R:E ─→ ℙ].`
`    ∀f:{e:E| P e}  ─→ {e:E| Q e} . ∀g:{e:E| Q e}  ─→ {e:E| R e} .  ((Q ←←= f== P ∧ R ←←= g== Q) `` R ←←= g o f== P)`

Proof

Definitions occuring in Statement :  weak-antecedent-surjection: `Q ←←= f== P` es-E: `E` event_ordering: `EO` compose: `f o g` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ─→ B[x]`
Lemmas :  weak-antecedent-functions-compose set_wf es-E_wf equal_wf compose_wf and_wf member_wf
\mforall{}es:EO
\mforall{}[P,Q,R:E  {}\mrightarrow{}  \mBbbP{}].
\mforall{}f:\{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  .  \mforall{}g:\{e:E|  Q  e\}    {}\mrightarrow{}  \{e:E|  R  e\}  .
((Q  \mleftarrow{}\mleftarrow{}=  f==  P  \mwedge{}  R  \mleftarrow{}\mleftarrow{}=  g==  Q)  {}\mRightarrow{}  R  \mleftarrow{}\mleftarrow{}=  g  o  f==  P)

Date html generated: 2015_07_17-AM-09_02_34
Last ObjectModification: 2015_01_27-PM-00_54_27

Home Index