---

Step * 2 1 2 1 1 7 1 3 of Lemma Q-R-glued-first

.....antecedent..... 
1. Info : Type
2. es : EO+(Info)@i'
3. Q : E ─→ E ─→ ℙ
4. R : E ─→ E ─→ ℙ
5. A : Type
6. B : Type
7. Ia1 : EClass(A)@i'
8. Iaa : EClass(A) List@i'
9. ∀Ibs:EClass(B) List. ∀f:E(first-class(Iaa)) ─→ B.
     ((∀i:ℕ||Iaa||. Iaa[i]:Q →─f─→  Ibs[i]:R)
        ⇒ first-class(Iaa):Q →─f─→  first-class(Ibs):R 
           supposing (∀Ia1,Ia2∈Iaa.  ∀e,e':E.
                                       ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposing 
        ((||Iaa|| = ||Ibs|| ∈ ℤ) and 
        (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0) and 
        (∀Ia1,Ia2∈Iaa.  Ia1 ∩ Ia2 = 0))@i 2
10. Ib1 : EClass(B)
11. Ibb : EClass(B) List
12. f : E(first-class([Ia1 / Iaa])) ─→ B@i
13. (∀Ia1,Ia2∈[Ia1 / Iaa].  Ia1 ∩ Ia2 = 0)
14. (∀Ib1,Ib2∈[Ib1 / Ibb].  Ib1 ∩ Ib2 = 0)
15. ||[Ia1 / Iaa]|| = ||[Ib1 / Ibb]|| ∈ ℤ
16. ∀i:ℕ||[Ia1 / Iaa]||. [Ia1 / Iaa][i]:Q →─f─→  [Ib1 / Ibb][i]:R@i
17. (∀Ia1,Ia2∈[Ia1 / Iaa].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
18. first-class(Iaa):Q →─f─→  first-class(Ibb):R
19. Ia1:Q →─f─→  Ib1:R
⊢ Ib1 ∩ first-class(Ibb) = 0
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN D (-1)
   THEN ((RWO "is-first-class" (-1)) THENA Auto)
   THEN (RWO "l_exists_iff" (-1) THENA Auto)
   THEN ExRepD
   THEN OnMaybeHyp 14 (\h. ((RWO "pairwise-cons" h THENA Auto)
                            THEN Auto
                            THEN (RWO "l_all_iff" (h+1) THENA Auto)
                            THEN ((InstHyp [⌈X⌉] (h+1))⋅ THENA Auto)
                            THEN ((UnfoldTopAb (-1)) THEN ((InstHyp [⌈e1⌉;⌈e⌉] (-1))⋅ THENM D -1) THEN Complete (Auto))
                            ⋅))⋅) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  Q  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  R  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  A  :  Type
6.  B  :  Type
7.  Ia1  :  EClass(A)@i'
8.  Iaa  :  EClass(A)  List@i'
9.  \mforall{}Ibs:EClass(B)  List.  \mforall{}f:E(first-class(Iaa))  {}\mrightarrow{}  B.
          ((\mforall{}i:\mBbbN{}||Iaa||.  Iaa[i]:Q  \mrightarrow{}{}f{}\mrightarrow{}    Ibs[i]:R)
                {}\mRightarrow{}  first-class(Iaa):Q  \mrightarrow{}{}f{}\mrightarrow{}    first-class(Ibs):R 
                      supposing  (\mforall{}Ia1,Ia2\mmember{}Iaa.    \mforall{}e,e':E.
                                                                              ((\mneg{}(Q  e  e'))  \mwedge{}  (\mneg{}(Q  e'  e)))  supposing 
                                                                                    ((\muparrow{}e'  \mmember{}\msubb{}  Ia2)  and 
                                                                                    (\muparrow{}e  \mmember{}\msubb{}  Ia1))))  supposing 
                ((||Iaa||  =  ||Ibs||)  and 
                (\mforall{}Ib1,Ib2\mmember{}Ibs.    Ib1  \mcap{}  Ib2  =  0)  and 
                (\mforall{}Ia1,Ia2\mmember{}Iaa.    Ia1  \mcap{}  Ia2  =  0))@i  2
10.  Ib1  :  EClass(B)
11.  Ibb  :  EClass(B)  List
12.  f  :  E(first-class([Ia1  /  Iaa]))  {}\mrightarrow{}  B@i
13.  (\mforall{}Ia1,Ia2\mmember{}[Ia1  /  Iaa].    Ia1  \mcap{}  Ia2  =  0)
14.  (\mforall{}Ib1,Ib2\mmember{}[Ib1  /  Ibb].    Ib1  \mcap{}  Ib2  =  0)
15.  ||[Ia1  /  Iaa]||  =  ||[Ib1  /  Ibb]||
16.  \mforall{}i:\mBbbN{}||[Ia1  /  Iaa]||.  [Ia1  /  Iaa][i]:Q  \mrightarrow{}{}f{}\mrightarrow{}    [Ib1  /  Ibb][i]:R@i
17.  (\mforall{}Ia1,Ia2\mmember{}[Ia1  /  Iaa].    \mforall{}e,e':E.
                                                            ((\mneg{}(Q  e  e'))  \mwedge{}  (\mneg{}(Q  e'  e)))  supposing  ((\muparrow{}e'  \mmember{}\msubb{}  Ia2)  and  (\muparrow{}e  \mmember{}\msubb{}  Ia1)))
18.  first-class(Iaa):Q  \mrightarrow{}{}f{}\mrightarrow{}    first-class(Ibb):R
19.  Ia1:Q  \mrightarrow{}{}f{}\mrightarrow{}    Ib1:R
\mvdash{}  Ib1  \mcap{}  first-class(Ibb)  =  0


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  D  (-1)
  THEN  ((RWO  "is-first-class"  (-1))  THENA  Auto)
  THEN  (RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  OnMaybeHyp  14  (\mbackslash{}h.  ((RWO  "pairwise-cons"  h  THENA  Auto)
                                                    THEN  Auto
                                                    THEN  (RWO  "l\_all\_iff"  (h+1)  THENA  Auto)
                                                    THEN  ((InstHyp  [\mkleeneopen{}X\mkleeneclose{}]  (h+1))\mcdot{}  THENA  Auto)
                                                    THEN  ((UnfoldTopAb  (-1))
                                                                THEN  ((InstHyp  [\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  (-1))\mcdot{}  THENM  D  -1)
                                                                THEN  Complete  (Auto))\mcdot{}))\mcdot{})

---

Home Index