Definition df-mntop 33302

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

Assertion

Ref	Expression
df-mntop	⊢ ManTop = {⟨𝑛, 𝑗⟩ ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))}

Distinct variable group:   𝑗,𝑛

Detailed syntax breakdown of Definition df-mntop

Step	Hyp	Ref	Expression
1		cmntop 33301	. 2 class ManTop
2		vn	. . . . . 6 setvar 𝑛
3	2	cv 1539	. . . . 5 class 𝑛
4		cn0 12477	. . . . 5 class ℕ0
5	3, 4	wcel 2105	. . . 4 wff 𝑛 ∈ ℕ0
6		vj	. . . . . . 7 setvar 𝑗
7	6	cv 1539	. . . . . 6 class 𝑗
8		c2ndc 23163	. . . . . 6 class 2ndω
9	7, 8	wcel 2105	. . . . 5 wff 𝑗 ∈ 2ndω
10		cha 23033	. . . . . 6 class Haus
11	7, 10	wcel 2105	. . . . 5 wff 𝑗 ∈ Haus
12		cehl 25133	. . . . . . . . . 10 class 𝔼hil
13	3, 12	cfv 6543	. . . . . . . . 9 class (𝔼hil‘𝑛)
14		ctopn 17372	. . . . . . . . 9 class TopOpen
15	13, 14	cfv 6543	. . . . . . . 8 class (TopOpen‘(𝔼hil‘𝑛))
16		chmph 23479	. . . . . . . 8 class ≃
17	15, 16	cec 8704	. . . . . . 7 class [(TopOpen‘(𝔼hil‘𝑛))] ≃
18	17	clly 23189	. . . . . 6 class Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃
19	7, 18	wcel 2105	. . . . 5 wff 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃
20	9, 11, 19	w3a 1086	. . . 4 wff (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ )
21	5, 20	wa 395	. . 3 wff (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))
22	21, 2, 6	copab 5210	. 2 class {⟨𝑛, 𝑗⟩ ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))}
23	1, 22	wceq 1540	1 wff ManTop = {⟨𝑛, 𝑗⟩ ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))}

This definition is referenced by:  relmntop  33303  ismntoplly  33304