Metamath Proof Explorer


Definition df-mntop

Description: Define the class of N -manifold topologies, as second 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 ) ) ] ~= ) ) }