Proof of Nuprl Lemma : Q-R-glues-conditional

Step * 1 of Lemma Q-R-glues-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. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. g1 glues Ia1:Q1 ──f─→ Ib1:R@i
18. g2 glues Ia2:Q2 ──f─→ Ib2:R@i
⊢ [{Ib1}? g1 : g2] glues [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} ──f─→ [Ib1?Ib2]:R
BY
{ (All (Unfold `Q-R-glues`) 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. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. {Ia1} ←←= g1== {Ib1}@i
18. g1 is Q1-R-pre-preserving on {Ib1}@i
19. Inj(E(Ib1);E;g1)@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. {Ia2} ←←= g2== {Ib2}@i
22. g2 is Q2-R-pre-preserving on {Ib2}@i
23. Inj(E(Ib2);E;g2)@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
⊢ {[Ia1?Ia2]} ←←= [{Ib1}? g1 : g2]== {[Ib1?Ib2]}

2
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. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. {Ia1} ←←= g1== {Ib1}@i
18. g1 is Q1-R-pre-preserving on {Ib1}@i
19. Inj(E(Ib1);E;g1)@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. {Ia2} ←←= g2== {Ib2}@i
22. g2 is Q2-R-pre-preserving on {Ib2}@i
23. Inj(E(Ib2);E;g2)@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
25. {[Ia1?Ia2]} ←←= [{Ib1}? g1 : g2]== {[Ib1?Ib2]}
⊢ [{Ib1}? g1 : g2] is Q1|{Ia1} ∨ Q2|{Ia2}-R-pre-preserving on {[Ib1?Ib2]}

3
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. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. {Ia1} ←←= g1== {Ib1}@i
18. g1 is Q1-R-pre-preserving on {Ib1}@i
19. Inj(E(Ib1);E;g1)@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. {Ia2} ←←= g2== {Ib2}@i
22. g2 is Q2-R-pre-preserving on {Ib2}@i
23. Inj(E(Ib2);E;g2)@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
25. {[Ia1?Ia2]} ←←= [{Ib1}? g1 : g2]== {[Ib1?Ib2]}
26. [{Ib1}? g1 : g2] is Q1|{Ia1} ∨ Q2|{Ia2}-R-pre-preserving on {[Ib1?Ib2]}
⊢ Inj(E([Ib1?Ib2]);E;[{Ib1}? g1 : g2])

4
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. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. {Ia1} ←←= g1== {Ib1}@i
18. g1 is Q1-R-pre-preserving on {Ib1}@i
19. Inj(E(Ib1);E;g1)@i
20. ∀e:E(Ib1). ((f (g1 e)) = Ib1(e) ∈ B)@i
21. {Ia2} ←←= g2== {Ib2}@i
22. g2 is Q2-R-pre-preserving on {Ib2}@i
23. Inj(E(Ib2);E;g2)@i
24. ∀e:E(Ib2). ((f (g2 e)) = Ib2(e) ∈ B)@i
25. {[Ia1?Ia2]} ←←= [{Ib1}? g1 : g2]== {[Ib1?Ib2]}
26. [{Ib1}? g1 : g2] is Q1|{Ia1} ∨ Q2|{Ia2}-R-pre-preserving on {[Ib1?Ib2]}
27. Inj(E([Ib1?Ib2]);E;[{Ib1}? g1 : g2])
28. e : E([Ib1?Ib2])@i
⊢ (f ([{Ib1}? g1 : g2] e)) = [Ib1?Ib2](e) ∈ B

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. g1 : E(Ib1) {}\mrightarrow{} E(Ia1)@i 14. g2 : E(Ib2) {}\mrightarrow{} E(Ia2)@i 15. Ia1 \mcap{} Ia2 = 0 16. Ib1 \mcap{} Ib2 = 0 17. g1 glues Ia1:Q1 {}{}f{}\mrightarrow{} Ib1:R@i 18. g2 glues Ia2:Q2 {}{}f{}\mrightarrow{} Ib2:R@i \mvdash{} [\{Ib1\}? g1 : g2] glues [Ia1?Ia2]:Q1|\{Ia1\} \mvee{} Q2|\{Ia2\} {}{}f{}\mrightarrow{} [Ib1?Ib2]:R By Latex: (All (Unfold `Q-R-glues`) THEN Auto)\mcdot{} Home Index