---

Step * 1 1 of Lemma Q-R-glued-conditional


1. [Info] : Type
2. es : EO+(Info)@i'
3. [Q1] : E ─→ E ─→ ℙ
4. [Q2] : E ─→ E ─→ ℙ
5. [R] : E ─→ E ─→ ℙ
6. [A] : Type
7. [B] : Type
8. Ia1 : EClass(A)@i'
9. Ia2 : EClass(A)@i'
10. Ib1 : EClass(B)@i'
11. Ib2 : EClass(B)@i'
12. f : E([Ia1?Ia2]) ─→ B@i
13. Ia1 ∩ Ia2 = 0
14. Ib1 ∩ Ib2 = 0
15. g1 : E(Ib1) ─→ E@i
16. g1 glues Ia1:Q1 ──f─→ Ib1:R@i
17. g : E(Ib2) ─→ E@i
18. g glues Ia2:Q2 ──f─→ Ib2:R@i
19. [Ia1?Ia2] ∈ EClass(A)
20. E(Ia1) ⊆r E([Ia1?Ia2])
21. g ∈ E(Ib2) ─→ E(Ia2)
22. g1 ∈ E(Ib1) ─→ E(Ia1)
⊢ [{Ib1}? g1 : g] glues [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} ──f─→ [Ib1?Ib2]:R
BY
{ (BLemma `Q-R-glues-conditional` THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [Q1]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  [Q2]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  [R]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
6.  [A]  :  Type
7.  [B]  :  Type
8.  Ia1  :  EClass(A)@i'
9.  Ia2  :  EClass(A)@i'
10.  Ib1  :  EClass(B)@i'
11.  Ib2  :  EClass(B)@i'
12.  f  :  E([Ia1?Ia2])  {}\mrightarrow{}  B@i
13.  Ia1  \mcap{}  Ia2  =  0
14.  Ib1  \mcap{}  Ib2  =  0
15.  g1  :  E(Ib1)  {}\mrightarrow{}  E@i
16.  g1  glues  Ia1:Q1  {}{}f{}\mrightarrow{}  Ib1:R@i
17.  g  :  E(Ib2)  {}\mrightarrow{}  E@i
18.  g  glues  Ia2:Q2  {}{}f{}\mrightarrow{}  Ib2:R@i
19.  [Ia1?Ia2]  \mmember{}  EClass(A)
20.  E(Ia1)  \msubseteq{}r  E([Ia1?Ia2])
21.  g  \mmember{}  E(Ib2)  {}\mrightarrow{}  E(Ia2)
22.  g1  \mmember{}  E(Ib1)  {}\mrightarrow{}  E(Ia1)
\mvdash{}  [\{Ib1\}?  g1  :  g]  glues  [Ia1?Ia2]:Q1|\{Ia1\}  \mvee{}  Q2|\{Ia2\}  {}{}f{}\mrightarrow{}  [Ib1?Ib2]:R


By

---

Latex:
(BLemma  `Q-R-glues-conditional`  THEN  Auto)\mcdot{}

---

Home Index