Definition df-mntop 30067

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.)

Assertion

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

Distinct variable group:   j, n

Detailed syntax breakdown of Definition df-mntop

Step	Hyp	Ref	Expression
1		cmntop 30066	. 2 class ManTop
2		vn	. . . . . 6 setvar n
3	2	cv 1482	. . . . 5 class n
4		cn0 11292	. . . . 5 class NN0
5	3, 4	wcel 1990	. . . 4 wff n e. NN0
6		vj	. . . . . . 7 setvar j
7	6	cv 1482	. . . . . 6 class j
8		c2ndc 21241	. . . . . 6 class 2ndc
9	7, 8	wcel 1990	. . . . 5 wff j e. 2ndc
10		cha 21112	. . . . . 6 class Haus
11	7, 10	wcel 1990	. . . . 5 wff j e. Haus
12		cehl 23172	. . . . . . . . . 10 class 𝔼hil
13	3, 12	cfv 5888	. . . . . . . . 9 class (𝔼hil ` n )
14		ctopn 16082	. . . . . . . . 9 class TopOpen
15	13, 14	cfv 5888	. . . . . . . 8 class ( TopOpen ` (𝔼hil ` n ) )
16		chmph 21557	. . . . . . . 8 class ~=
17	15, 16	cec 7740	. . . . . . 7 class [ ( TopOpen ` (𝔼hil ` n ) ) ] ~=
18	17	clly 21267	. . . . . 6 class Locally [ ( TopOpen ` (𝔼hil ` n ) ) ] ~=
19	7, 18	wcel 1990	. . . . 5 wff j e. Locally [ ( TopOpen ` (𝔼hil ` n ) ) ] ~=
20	9, 11, 19	w3a 1037	. . . 4 wff ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` (𝔼hil ` n ) ) ] ~= )
21	5, 20	wa 384	. . 3 wff ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` (𝔼hil ` n ) ) ] ~= ) )
22	21, 2, 6	copab 4712	. 2 class { <. n , j >. | ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` (𝔼hil ` n ) ) ] ~= ) ) }
23	1, 22	wceq 1483	1 wff ManTop = { <. n , j >. | ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` (𝔼hil ` n ) ) ] ~= ) ) }

This definition is referenced by:  relmntop  30068  ismntoplly  30069