---

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


1. [Info] : Type
2. es : EO+(Info)@i'
3. [Q] : E ─→ E ─→ ℙ
4. [R] : E ─→ E ─→ ℙ
5. [A] : Type
6. [B] : Type
7. u : EClass(A)@i'
8. v : EClass(A) List@i'
9. ∀Ibs:EClass(B) List. ∀f:E(first-class(v)) ─→ B.
     ((∀i:ℕ||v||. v[i]:Q →─f─→  Ibs[i]:R)
        ⇒ first-class(v):Q →─f─→  first-class(Ibs):R 
           supposing (∀Ia1,Ia2∈v.  ∀e,e':E.
                                     ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposing 
        ((||v|| = ||Ibs|| ∈ ℤ) and 
        (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0) and 
        (∀Ia1,Ia2∈v.  Ia1 ∩ Ia2 = 0))@i 2
10. Ibs : EClass(B) List@i'
11. f : E(first-class([u / v])) ─→ B@i
12. (∀Ia1,Ia2∈[u / v].  Ia1 ∩ Ia2 = 0)
13. (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0)
14. ||[u / v]|| = ||Ibs|| ∈ ℤ
15. ∀i:ℕ||[u / v]||. [u / v][i]:Q →─f─→  Ibs[i]:R@i
16. (∀Ia1,Ia2∈[u / v].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
⊢ first-class([u / v]):Q →─f─→  first-class(Ibs):R
BY
{ DVar `Ibs' }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [Q] : E ─→ E ─→ ℙ
4. [R] : E ─→ E ─→ ℙ
5. [A] : Type
6. [B] : Type
7. u : EClass(A)@i'
8. v : EClass(A) List@i'
9. ∀Ibs:EClass(B) List. ∀f:E(first-class(v)) ─→ B.
     ((∀i:ℕ||v||. v[i]:Q →─f─→  Ibs[i]:R)
        ⇒ first-class(v):Q →─f─→  first-class(Ibs):R 
           supposing (∀Ia1,Ia2∈v.  ∀e,e':E.
                                     ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposing 
        ((||v|| = ||Ibs|| ∈ ℤ) and 
        (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0) and 
        (∀Ia1,Ia2∈v.  Ia1 ∩ Ia2 = 0))@i 2
10. f : E(first-class([u / v])) ─→ B@i
11. (∀Ia1,Ia2∈[u / v].  Ia1 ∩ Ia2 = 0)
12. (∀Ib1,Ib2∈[].  Ib1 ∩ Ib2 = 0)
13. ||[u / v]|| = ||[]|| ∈ ℤ
14. ∀i:ℕ||[u / v]||. [u / v][i]:Q →─f─→  [][i]:R@i
15. (∀Ia1,Ia2∈[u / v].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
⊢ first-class([u / v]):Q →─f─→  first-class([]):R

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. [Q] : E ─→ E ─→ ℙ
4. [R] : E ─→ E ─→ ℙ
5. [A] : Type
6. [B] : Type
7. u : EClass(A)@i'
8. v : EClass(A) List@i'
9. ∀Ibs:EClass(B) List. ∀f:E(first-class(v)) ─→ B.
     ((∀i:ℕ||v||. v[i]:Q →─f─→  Ibs[i]:R)
        ⇒ first-class(v):Q →─f─→  first-class(Ibs):R 
           supposing (∀Ia1,Ia2∈v.  ∀e,e':E.
                                     ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposing 
        ((||v|| = ||Ibs|| ∈ ℤ) and 
        (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0) and 
        (∀Ia1,Ia2∈v.  Ia1 ∩ Ia2 = 0))@i 2
10. u1 : EClass(B)
11. v1 : EClass(B) List
12. f : E(first-class([u / v])) ─→ B@i
13. (∀Ia1,Ia2∈[u / v].  Ia1 ∩ Ia2 = 0)
14. (∀Ib1,Ib2∈[u1 / v1].  Ib1 ∩ Ib2 = 0)
15. ||[u / v]|| = ||[u1 / v1]|| ∈ ℤ
16. ∀i:ℕ||[u / v]||. [u / v][i]:Q →─f─→  [u1 / v1][i]:R@i
17. (∀Ia1,Ia2∈[u / v].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
⊢ first-class([u / v]):Q →─f─→  first-class([u1 / v1]):R

---

Latex:

---

Latex:

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.  u  :  EClass(A)@i'
8.  v  :  EClass(A)  List@i'
9.  \mforall{}Ibs:EClass(B)  List.  \mforall{}f:E(first-class(v))  {}\mrightarrow{}  B.
          ((\mforall{}i:\mBbbN{}||v||.  v[i]:Q  \mrightarrow{}{}f{}\mrightarrow{}    Ibs[i]:R)
                {}\mRightarrow{}  first-class(v):Q  \mrightarrow{}{}f{}\mrightarrow{}    first-class(Ibs):R 
                      supposing  (\mforall{}Ia1,Ia2\mmember{}v.    \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 
                ((||v||  =  ||Ibs||)  and 
                (\mforall{}Ib1,Ib2\mmember{}Ibs.    Ib1  \mcap{}  Ib2  =  0)  and 
                (\mforall{}Ia1,Ia2\mmember{}v.    Ia1  \mcap{}  Ia2  =  0))@i  2
10.  Ibs  :  EClass(B)  List@i'
11.  f  :  E(first-class([u  /  v]))  {}\mrightarrow{}  B@i
12.  (\mforall{}Ia1,Ia2\mmember{}[u  /  v].    Ia1  \mcap{}  Ia2  =  0)
13.  (\mforall{}Ib1,Ib2\mmember{}Ibs.    Ib1  \mcap{}  Ib2  =  0)
14.  ||[u  /  v]||  =  ||Ibs||
15.  \mforall{}i:\mBbbN{}||[u  /  v]||.  [u  /  v][i]:Q  \mrightarrow{}{}f{}\mrightarrow{}    Ibs[i]:R@i
16.  (\mforall{}Ia1,Ia2\mmember{}[u  /  v].    \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)))
\mvdash{}  first-class([u  /  v]):Q  \mrightarrow{}{}f{}\mrightarrow{}    first-class(Ibs):R


By

---

Latex:
DVar  `Ibs'

---

Home Index