Proof of Nuprl Lemma : Q-R-glued-first

Step * 2 1 2 1 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. 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)))

⊢ [Ia1?first-class(Iaa)]:Q →─f─→  [Ib1?first-class(Ibb)]:R
BY
{ ((InstHyp [⌈Ibb⌉; ⌈f⌉] 9)⋅ THENA (Auto THEN Auto)) }

1
.....wf.....
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

17. (∀Ia1,Ia2∈[Ia1 / Iaa].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈_b Ia2) and (↑e ∈_b Ia1)))

⊢ f ∈ E(first-class(Iaa)) ─→ B

2
.....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

17. (∀Ia1,Ia2∈[Ia1 / Iaa].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈_b Ia2) and (↑e ∈_b Ia1)))

⊢ (∀Ia1,Ia2∈Iaa.  Ia1 ∩ Ia2 = 0)

3
.....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

17. (∀Ia1,Ia2∈[Ia1 / Iaa].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈_b Ia2) and (↑e ∈_b Ia1)))

⊢ (∀Ib1,Ib2∈Ibb.  Ib1 ∩ Ib2 = 0)

4
.....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

17. (∀Ia1,Ia2∈[Ia1 / Iaa].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈_b Ia2) and (↑e ∈_b Ia1)))

⊢ ||Iaa|| = ||Ibb|| ∈ ℤ

5
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

17. (∀Ia1,Ia2∈[Ia1 / Iaa].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈_b Ia2) and (↑e ∈_b Ia1)))

18. i : ℕ||Iaa||@i
⊢ Iaa[i]:Q →─f─→  Ibb[i]:R

6
.....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

17. (∀Ia1,Ia2∈[Ia1 / Iaa].  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈_b Ia2) and (↑e ∈_b Ia1)))

⊢ (∀Ia1,Ia2∈Iaa.  ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈_b Ia2) and (↑e ∈_b Ia1)))

7
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

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
⊢ [Ia1?first-class(Iaa)]:Q →─f─→ [Ib1?first-class(Ibb)]: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. 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))) \mvdash{} [Ia1?first-class(Iaa)]:Q \mrightarrow{}{}f{}\mrightarrow{} [Ib1?first-class(Ibb)]:R By Latex: ((InstHyp [\mkleeneopen{}Ibb\mkleeneclose{}; \mkleeneopen{}f\mkleeneclose{}] 9)\mcdot{} THENA (Auto THEN Auto)) Home Index