---

Step * 1 of Lemma weak-antecedent-surjections-compose


1. es : EO@i'
2. [P] : E ─→ ℙ
3. [Q] : E ─→ ℙ
4. [R] : E ─→ ℙ
5. f : {e:E| P e}  ─→ {e:E| Q e} @i
6. g : {e:E| Q e}  ─→ {e:E| R e} @i
7. Q ←←= f== P@i
8. R ←←= g== Q@i
⊢ R ←←= g o f== P
BY
{ ((All (Unfold `weak-antecedent-surjection`) THEN SplitAndHyps) THEN D 0) }

1
1. es : EO@i'
2. [P] : E ─→ ℙ
3. [Q] : E ─→ ℙ
4. [R] : E ─→ ℙ
5. f : {e:E| P e}  ─→ {e:E| Q e} @i
6. g : {e:E| Q e}  ─→ {e:E| R e} @i
7. Q ←==f== P@i
8. ∀e:{e:E| Q e} . ∃e':{e:E| P e} . ((f e') = e ∈ E)@i
9. R ←==g== Q@i
10. ∀e:{e:E| R e} . ∃e':{e:E| Q e} . ((g e') = e ∈ E)@i
⊢ R ←==g o f== P

2
1. es : EO@i'
2. [P] : E ─→ ℙ
3. [Q] : E ─→ ℙ
4. [R] : E ─→ ℙ
5. f : {e:E| P e}  ─→ {e:E| Q e} @i
6. g : {e:E| Q e}  ─→ {e:E| R e} @i
7. Q ←==f== P@i
8. ∀e:{e:E| Q e} . ∃e':{e:E| P e} . ((f e') = e ∈ E)@i
9. R ←==g== Q@i
10. ∀e:{e:E| R e} . ∃e':{e:E| Q e} . ((g e') = e ∈ E)@i
⊢ ∀e:{e:E| R e} . ∃e':{e:E| P e} . (((g o f) e') = e ∈ E)

---

Latex:



1.  es  :  EO@i'
2.  [P]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  [R]  :  E  {}\mrightarrow{}  \mBbbP{}
5.  f  :  \{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  @i
6.  g  :  \{e:E|  Q  e\}    {}\mrightarrow{}  \{e:E|  R  e\}  @i
7.  Q  \mleftarrow{}\mleftarrow{}=  f==  P@i
8.  R  \mleftarrow{}\mleftarrow{}=  g==  Q@i
\mvdash{}  R  \mleftarrow{}\mleftarrow{}=  g  o  f==  P


By

((All  (Unfold  `weak-antecedent-surjection`)  THEN  SplitAndHyps)  THEN  D  0)

---

Home Index