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 = { ⟨ 𝑛 , 𝑗 ⟩ ∣ ( 𝑛 ∈ ℕ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𝑛 ) ) ] ≃ ) ) }