---

Step * 3 1 1 1 of Lemma Q-R-glues-composes


1. Info : Type
2. es : EO+(Info)@i'
3. Qa : E ─→ E ─→ ℙ
4. Rb : E ─→ E ─→ ℙ
5. Sc : E ─→ E ─→ ℙ
6. A : Type
7. B : Type
8. C : Type
9. Ia : EClass(A)@i'
10. Ib : EClass(B)@i'
11. Ic : EClass(C)@i'
12. f1 : E(Ia) ─→ B@i
13. f2 : B ─→ C@i
14. g1 : E(Ib) ─→ E(Ia)@i
15. g2 : E(Ic) ─→ E(Ib)@i
16. λe.(↑e ∈b Ia) ←←= g1== λe.(↑e ∈b Ib)@i
17. g1 is Qa-Rb-pre-preserving on λe.(↑e ∈b Ib)@i
18. Inj(E(Ib);E;g1)@i
19. ∀e:E(Ib). ((f1 (g1 e)) = Ib(e) ∈ B)@i
20. λe.(↑e ∈b Ib) ←←= g2== λe.(↑e ∈b Ic)@i
21. g2 is Rb-Sc-pre-preserving on λe.(↑e ∈b Ic)@i
22. Inj(E(Ic);E;g2)@i
23. ∀e:E(Ic). ((f2 Ib(g2 e)) = Ic(e) ∈ C)@i
24. λe.(↑e ∈b Ia) ←←= g1 o g2== λe.(↑e ∈b Ic)
25. g1 o g2 is Qa-Sc-pre-preserving on λe.(↑e ∈b Ic)
⊢ Inj(E(Ic);E(Ib);g2)
BY
{ MoveToHyp 0 (-4) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. Qa : E ─→ E ─→ ℙ
4. Rb : E ─→ E ─→ ℙ
5. Sc : E ─→ E ─→ ℙ
6. A : Type
7. B : Type
8. C : Type
9. Ia : EClass(A)@i'
10. Ib : EClass(B)@i'
11. Ic : EClass(C)@i'
12. f1 : E(Ia) ─→ B@i
13. f2 : B ─→ C@i
14. g1 : E(Ib) ─→ E(Ia)@i
15. g2 : E(Ic) ─→ E(Ib)@i
16. λe.(↑e ∈b Ia) ←←= g1== λe.(↑e ∈b Ib)@i
17. g1 is Qa-Rb-pre-preserving on λe.(↑e ∈b Ib)@i
18. Inj(E(Ib);E;g1)@i
19. ∀e:E(Ib). ((f1 (g1 e)) = Ib(e) ∈ B)@i
20. λe.(↑e ∈b Ib) ←←= g2== λe.(↑e ∈b Ic)@i
21. g2 is Rb-Sc-pre-preserving on λe.(↑e ∈b Ic)@i
22. ∀e:E(Ic). ((f2 Ib(g2 e)) = Ic(e) ∈ C)@i
23. λe.(↑e ∈b Ia) ←←= g1 o g2== λe.(↑e ∈b Ic)
24. g1 o g2 is Qa-Sc-pre-preserving on λe.(↑e ∈b Ic)
25. Inj(E(Ic);E;g2)
⊢ Inj(E(Ic);E(Ib);g2)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  Qa  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  Rb  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  Sc  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
6.  A  :  Type
7.  B  :  Type
8.  C  :  Type
9.  Ia  :  EClass(A)@i'
10.  Ib  :  EClass(B)@i'
11.  Ic  :  EClass(C)@i'
12.  f1  :  E(Ia)  {}\mrightarrow{}  B@i
13.  f2  :  B  {}\mrightarrow{}  C@i
14.  g1  :  E(Ib)  {}\mrightarrow{}  E(Ia)@i
15.  g2  :  E(Ic)  {}\mrightarrow{}  E(Ib)@i
16.  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ia)  \mleftarrow{}\mleftarrow{}=  g1==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)@i
17.  g1  is  Qa-Rb-pre-preserving  on  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)@i
18.  Inj(E(Ib);E;g1)@i
19.  \mforall{}e:E(Ib).  ((f1  (g1  e))  =  Ib(e))@i
20.  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)  \mleftarrow{}\mleftarrow{}=  g2==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)@i
21.  g2  is  Rb-Sc-pre-preserving  on  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)@i
22.  Inj(E(Ic);E;g2)@i
23.  \mforall{}e:E(Ic).  ((f2  Ib(g2  e))  =  Ic(e))@i
24.  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ia)  \mleftarrow{}\mleftarrow{}=  g1  o  g2==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)
25.  g1  o  g2  is  Qa-Sc-pre-preserving  on  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)
\mvdash{}  Inj(E(Ic);E(Ib);g2)


By

---

Latex:
MoveToHyp  0  (-4)

---

Home Index