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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmntop	⊢ ManTop
1		vn	⊢ 𝑛
2		vj	⊢ 𝑗
3	1	cv	⊢ 𝑛
4		cn0	⊢ ℕ0
5	3 4	wcel	⊢ 𝑛 ∈ ℕ0
6	2	cv	⊢ 𝑗
7		c2ndc	⊢ 2ndω
8	6 7	wcel	⊢ 𝑗 ∈ 2ndω
9		cha	⊢ Haus
10	6 9	wcel	⊢ 𝑗 ∈ Haus
11		ctopn	⊢ TopOpen
12		cehl	⊢ 𝔼hil
13	3 12	cfv	⊢ ( 𝔼hil ‘ 𝑛 )
14	13 11	cfv	⊢ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) )
15		chmph	⊢ ≃
16	14 15	cec	⊢ [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃
17	16	clly	⊢ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃
18	6 17	wcel	⊢ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃
19	8 10 18	w3a	⊢ ( 𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ )
20	5 19	wa	⊢ ( 𝑛 ∈ ℕ0 ∧ ( 𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ ) )
21	20 1 2	copab	⊢ { ⟨ 𝑛 , 𝑗 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ ( 𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ ) ) }
22	0 21	wceq	⊢ ManTop = { ⟨ 𝑛 , 𝑗 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ ( 𝑗 ∈ 2ndω ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [ ( TopOpen ‘ ( 𝔼hil ‘ 𝑛 ) ) ] ≃ ) ) }