Metamath Proof Explorer

Definition df-mntop

Description: Define the class of N-manifold topologies, as 2nd countable, Hausdorff topologies, locally homeomorphic to a ball of the Euclidean space of dimension N. (Contributed by Thierry Arnoux, 22-Dec-2019)

Ref Expression
Assertion df-mntop 
|- ManTop = { <. n , j >. | ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= ) ) }

Detailed syntax breakdown

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 ) ) ] ~= ) ) }