Step |
Hyp |
Ref |
Expression |
0 |
|
comn |
⊢ Ω𝑛 |
1 |
|
vj |
⊢ 𝑗 |
2 |
|
ctop |
⊢ Top |
3 |
|
vy |
⊢ 𝑦 |
4 |
1
|
cv |
⊢ 𝑗 |
5 |
4
|
cuni |
⊢ ∪ 𝑗 |
6 |
|
cc0 |
⊢ 0 |
7 |
|
vx |
⊢ 𝑥 |
8 |
|
cvv |
⊢ V |
9 |
|
vp |
⊢ 𝑝 |
10 |
|
ctopn |
⊢ TopOpen |
11 |
|
c1st |
⊢ 1st |
12 |
7
|
cv |
⊢ 𝑥 |
13 |
12 11
|
cfv |
⊢ ( 1st ‘ 𝑥 ) |
14 |
13 10
|
cfv |
⊢ ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) |
15 |
|
comi |
⊢ Ω1 |
16 |
|
c2nd |
⊢ 2nd |
17 |
12 16
|
cfv |
⊢ ( 2nd ‘ 𝑥 ) |
18 |
14 17 15
|
co |
⊢ ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) |
19 |
|
cicc |
⊢ [,] |
20 |
|
c1 |
⊢ 1 |
21 |
6 20 19
|
co |
⊢ ( 0 [,] 1 ) |
22 |
17
|
csn |
⊢ { ( 2nd ‘ 𝑥 ) } |
23 |
21 22
|
cxp |
⊢ ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) |
24 |
18 23
|
cop |
⊢ 〈 ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) 〉 |
25 |
7 9 8 8 24
|
cmpo |
⊢ ( 𝑥 ∈ V , 𝑝 ∈ V ↦ 〈 ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) 〉 ) |
26 |
25 11
|
ccom |
⊢ ( ( 𝑥 ∈ V , 𝑝 ∈ V ↦ 〈 ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) 〉 ) ∘ 1st ) |
27 |
|
cbs |
⊢ Base |
28 |
|
cnx |
⊢ ndx |
29 |
28 27
|
cfv |
⊢ ( Base ‘ ndx ) |
30 |
29 5
|
cop |
⊢ 〈 ( Base ‘ ndx ) , ∪ 𝑗 〉 |
31 |
|
cts |
⊢ TopSet |
32 |
28 31
|
cfv |
⊢ ( TopSet ‘ ndx ) |
33 |
32 4
|
cop |
⊢ 〈 ( TopSet ‘ ndx ) , 𝑗 〉 |
34 |
30 33
|
cpr |
⊢ { 〈 ( Base ‘ ndx ) , ∪ 𝑗 〉 , 〈 ( TopSet ‘ ndx ) , 𝑗 〉 } |
35 |
3
|
cv |
⊢ 𝑦 |
36 |
34 35
|
cop |
⊢ 〈 { 〈 ( Base ‘ ndx ) , ∪ 𝑗 〉 , 〈 ( TopSet ‘ ndx ) , 𝑗 〉 } , 𝑦 〉 |
37 |
26 36 6
|
cseq |
⊢ seq 0 ( ( ( 𝑥 ∈ V , 𝑝 ∈ V ↦ 〈 ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) 〉 ) ∘ 1st ) , 〈 { 〈 ( Base ‘ ndx ) , ∪ 𝑗 〉 , 〈 ( TopSet ‘ ndx ) , 𝑗 〉 } , 𝑦 〉 ) |
38 |
1 3 2 5 37
|
cmpo |
⊢ ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ seq 0 ( ( ( 𝑥 ∈ V , 𝑝 ∈ V ↦ 〈 ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) 〉 ) ∘ 1st ) , 〈 { 〈 ( Base ‘ ndx ) , ∪ 𝑗 〉 , 〈 ( TopSet ‘ ndx ) , 𝑗 〉 } , 𝑦 〉 ) ) |
39 |
0 38
|
wceq |
⊢ Ω𝑛 = ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ seq 0 ( ( ( 𝑥 ∈ V , 𝑝 ∈ V ↦ 〈 ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) 〉 ) ∘ 1st ) , 〈 { 〈 ( Base ‘ ndx ) , ∪ 𝑗 〉 , 〈 ( TopSet ‘ ndx ) , 𝑗 〉 } , 𝑦 〉 ) ) |