Step |
Hyp |
Ref |
Expression |
0 |
|
cpin |
⊢ πn |
1 |
|
vj |
⊢ 𝑗 |
2 |
|
ctop |
⊢ Top |
3 |
|
vp |
⊢ 𝑝 |
4 |
1
|
cv |
⊢ 𝑗 |
5 |
4
|
cuni |
⊢ ∪ 𝑗 |
6 |
|
vn |
⊢ 𝑛 |
7 |
|
cn0 |
⊢ ℕ0 |
8 |
|
c1st |
⊢ 1st |
9 |
|
comn |
⊢ Ω𝑛 |
10 |
3
|
cv |
⊢ 𝑝 |
11 |
4 10 9
|
co |
⊢ ( 𝑗 Ω𝑛 𝑝 ) |
12 |
6
|
cv |
⊢ 𝑛 |
13 |
12 11
|
cfv |
⊢ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) |
14 |
13 8
|
cfv |
⊢ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) |
15 |
|
cqus |
⊢ /s |
16 |
|
cc0 |
⊢ 0 |
17 |
12 16
|
wceq |
⊢ 𝑛 = 0 |
18 |
|
vx |
⊢ 𝑥 |
19 |
|
vy |
⊢ 𝑦 |
20 |
|
vf |
⊢ 𝑓 |
21 |
|
cii |
⊢ II |
22 |
|
ccn |
⊢ Cn |
23 |
21 4 22
|
co |
⊢ ( II Cn 𝑗 ) |
24 |
20
|
cv |
⊢ 𝑓 |
25 |
16 24
|
cfv |
⊢ ( 𝑓 ‘ 0 ) |
26 |
18
|
cv |
⊢ 𝑥 |
27 |
25 26
|
wceq |
⊢ ( 𝑓 ‘ 0 ) = 𝑥 |
28 |
|
c1 |
⊢ 1 |
29 |
28 24
|
cfv |
⊢ ( 𝑓 ‘ 1 ) |
30 |
19
|
cv |
⊢ 𝑦 |
31 |
29 30
|
wceq |
⊢ ( 𝑓 ‘ 1 ) = 𝑦 |
32 |
27 31
|
wa |
⊢ ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) |
33 |
32 20 23
|
wrex |
⊢ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) |
34 |
33 18 19
|
copab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } |
35 |
|
cphtpc |
⊢ ≃ph |
36 |
|
ctopn |
⊢ TopOpen |
37 |
|
cmin |
⊢ − |
38 |
12 28 37
|
co |
⊢ ( 𝑛 − 1 ) |
39 |
38 11
|
cfv |
⊢ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) |
40 |
39 8
|
cfv |
⊢ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) |
41 |
40 36
|
cfv |
⊢ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) |
42 |
41 35
|
cfv |
⊢ ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) |
43 |
17 34 42
|
cif |
⊢ if ( 𝑛 = 0 , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) |
44 |
14 43 15
|
co |
⊢ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) |
45 |
6 7 44
|
cmpt |
⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) ) |
46 |
1 3 2 5 45
|
cmpo |
⊢ ( 𝑗 ∈ Top , 𝑝 ∈ ∪ 𝑗 ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) ) ) |
47 |
0 46
|
wceq |
⊢ πn = ( 𝑗 ∈ Top , 𝑝 ∈ ∪ 𝑗 ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) ) ) |