Step |
Hyp |
Ref |
Expression |
0 |
|
cmntop |
|- ManTop |
1 |
|
vn |
|- n |
2 |
|
vj |
|- j |
3 |
1
|
cv |
|- n |
4 |
|
cn0 |
|- NN0 |
5 |
3 4
|
wcel |
|- n e. NN0 |
6 |
2
|
cv |
|- j |
7 |
|
c2ndc |
|- 2ndc |
8 |
6 7
|
wcel |
|- j e. 2ndc |
9 |
|
cha |
|- Haus |
10 |
6 9
|
wcel |
|- j e. Haus |
11 |
|
ctopn |
|- TopOpen |
12 |
|
cehl |
|- EEhil |
13 |
3 12
|
cfv |
|- ( EEhil ` n ) |
14 |
13 11
|
cfv |
|- ( TopOpen ` ( EEhil ` n ) ) |
15 |
|
chmph |
|- ~= |
16 |
14 15
|
cec |
|- [ ( TopOpen ` ( EEhil ` n ) ) ] ~= |
17 |
16
|
clly |
|- Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= |
18 |
6 17
|
wcel |
|- j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= |
19 |
8 10 18
|
w3a |
|- ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= ) |
20 |
5 19
|
wa |
|- ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= ) ) |
21 |
20 1 2
|
copab |
|- { <. n , j >. | ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= ) ) } |
22 |
0 21
|
wceq |
|- ManTop = { <. n , j >. | ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= ) ) } |