Step |
Hyp |
Ref |
Expression |
0 |
|
cmntop |
⊢ ManTop |
1 |
|
vn |
⊢ 𝑛 |
2 |
|
vj |
⊢ 𝑗 |
3 |
1
|
cv |
⊢ 𝑛 |
4 |
|
cn0 |
⊢ ℕ0 |
5 |
3 4
|
wcel |
⊢ 𝑛 ∈ ℕ0 |
6 |
2
|
cv |
⊢ 𝑗 |
7 |
|
c2ndc |
⊢ 2ndω |
8 |
6 7
|
wcel |
⊢ 𝑗 ∈ 2ndω |
9 |
|
cha |
⊢ Haus |
10 |
6 9
|
wcel |
⊢ 𝑗 ∈ Haus |
11 |
|
ctopn |
⊢ TopOpen |
12 |
|
cehl |
⊢ 𝔼hil |
13 |
3 12
|
cfv |
⊢ ( 𝔼hil ‘ 𝑛 ) |
14 |
13 11
|
cfv |
⊢ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) |
15 |
|
chmph |
⊢ ≃ |
16 |
14 15
|
cec |
⊢ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ |
17 |
16
|
clly |
⊢ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ |
18 |
6 17
|
wcel |
⊢ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ |
19 |
8 10 18
|
w3a |
⊢ ( 𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ ) |
20 |
5 19
|
wa |
⊢ ( 𝑛 ∈ ℕ0 ∧ ( 𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ ) ) |
21 |
20 1 2
|
copab |
⊢ { 〈 𝑛 , 𝑗 〉 ∣ ( 𝑛 ∈ ℕ0 ∧ ( 𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ ) ) } |
22 |
0 21
|
wceq |
⊢ ManTop = { 〈 𝑛 , 𝑗 〉 ∣ ( 𝑛 ∈ ℕ0 ∧ ( 𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ ) ) } |