---

Step * of Lemma Q-R-glued-conditional

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[Q1,Q2,R:E ─→ E ─→ ℙ]. ∀[A,B:Type].
      ∀Ia1,Ia2:EClass(A). ∀Ib1,Ib2:EClass(B). ∀f:E([Ia1?Ia2]) ─→ B.
        (Ia1:Q1 →─f─→  Ib1:R ⇒ Ia2:Q2 →─f─→  Ib2:R ⇒ [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} →─f─→  [Ib1?Ib2]:R) supposing 
           (Ib1 ∩ Ib2 = 0 and 
           Ia1 ∩ Ia2 = 0)
BY
{ (Repeat ((D 0 THENA Complete (Auto)))
   THEN (Assert [Ia1?Ia2] ∈ EClass(A) BY
               Auto)
   THEN (Assert E(Ia1) ⊆r E([Ia1?Ia2]) BY
               (D 0
                THEN Auto
                THEN (All (Unfold `es-E-interface`))
                THEN D -1
                THEN MemTypeCD
                THEN Auto
                THEN RWO "es-interface-conditional-domain-iff" 0
                THEN Auto))
   THEN Auto
   THEN (All (Unfold `Q-R-glued`))
   THEN ExRepD
   THEN AllHyps h.((FLemma `Q-R-glues-property` [h]) THENA (Auto THEN D -1 THEN Unhide THEN Auto)) ) }

1
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)
⊢ ∃g:E([Ib1?Ib2]) ─→ E. g glues [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} ──f─→ [Ib1?Ib2]:R

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[Q1,Q2,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B:Type].
            \mforall{}Ia1,Ia2:EClass(A).  \mforall{}Ib1,Ib2:EClass(B).  \mforall{}f:E([Ia1?Ia2])  {}\mrightarrow{}  B.
                (Ia1:Q1  \mrightarrow{}{}f{}\mrightarrow{}    Ib1:R
                      {}\mRightarrow{}  Ia2:Q2  \mrightarrow{}{}f{}\mrightarrow{}    Ib2:R
                      {}\mRightarrow{}  [Ia1?Ia2]:Q1|\{Ia1\}  \mvee{}  Q2|\{Ia2\}  \mrightarrow{}{}f{}\mrightarrow{}    [Ib1?Ib2]:R)  supposing 
                      (Ib1  \mcap{}  Ib2  =  0  and 
                      Ia1  \mcap{}  Ia2  =  0)


By

---

Latex:
(Repeat  ((D  0  THENA  Complete  (Auto)))
  THEN  (Assert  [Ia1?Ia2]  \mmember{}  EClass(A)  BY
                          Auto)
  THEN  (Assert  E(Ia1)  \msubseteq{}r  E([Ia1?Ia2])  BY
                          (D  0
                            THEN  Auto
                            THEN  (All  (Unfold  `es-E-interface`))
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  RWO  "es-interface-conditional-domain-iff"  0
                            THEN  Auto))
  THEN  Auto
  THEN  (All  (Unfold  `Q-R-glued`))
  THEN  ExRepD
  THEN  AllHyps  h.((FLemma  `Q-R-glues-property`  [h])  THENA  (Auto  THEN  D  -1  THEN  Unhide  THEN  Auto))  )

---

Home Index