Definition df-mntop 31259

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 = {⟨𝑛, 𝑗⟩ ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))}

Distinct variable group:   𝑗,𝑛

Detailed syntax breakdown of Definition df-mntop

Step	Hyp	Ref	Expression
1		cmntop 31258	. 2 class ManTop
2		vn	. . . . . 6 setvar 𝑛
3	2	cv 1532	. . . . 5 class 𝑛
4		cn0 11891	. . . . 5 class ℕ0
5	3, 4	wcel 2110	. . . 4 wff 𝑛 ∈ ℕ0
6		vj	. . . . . . 7 setvar 𝑗
7	6	cv 1532	. . . . . 6 class 𝑗
8		c2ndc 22040	. . . . . 6 class 2ndω
9	7, 8	wcel 2110	. . . . 5 wff 𝑗 ∈ 2ndω
10		cha 21910	. . . . . 6 class Haus
11	7, 10	wcel 2110	. . . . 5 wff 𝑗 ∈ Haus
12		cehl 23981	. . . . . . . . . 10 class 𝔼hil
13	3, 12	cfv 6349	. . . . . . . . 9 class (𝔼hil‘𝑛)
14		ctopn 16689	. . . . . . . . 9 class TopOpen
15	13, 14	cfv 6349	. . . . . . . 8 class (TopOpen‘(𝔼hil‘𝑛))
16		chmph 22356	. . . . . . . 8 class ≃
17	15, 16	cec 8281	. . . . . . 7 class [(TopOpen‘(𝔼hil‘𝑛))] ≃
18	17	clly 22066	. . . . . 6 class Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃
19	7, 18	wcel 2110	. . . . 5 wff 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃
20	9, 11, 19	w3a 1083	. . . 4 wff (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ )
21	5, 20	wa 398	. . 3 wff (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))
22	21, 2, 6	copab 5120	. 2 class {⟨𝑛, 𝑗⟩ ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))}
23	1, 22	wceq 1533	1 wff ManTop = {⟨𝑛, 𝑗⟩ ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil‘𝑛))] ≃ ))}

This definition is referenced by:  relmntop  31260  ismntoplly  31261