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 = n j | n ∈ ℕ 0 ∧ j ∈ 2 nd 𝜔 ∧ j ∈ Haus ∧ j ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmntop class ManTop
1 vn setvar n
2 vj setvar j
3 1 cv setvar n
4 cn0 class ℕ 0
5 3 4 wcel wff n ∈ ℕ 0
6 2 cv setvar j
7 c2ndc class 2 nd 𝜔
8 6 7 wcel wff j ∈ 2 nd 𝜔
9 cha class Haus
10 6 9 wcel wff j ∈ Haus
11 ctopn class TopOpen
12 cehl class 𝔼 hil
13 3 12 cfv class 𝔼 hil ⁡ n
14 13 11 cfv class TopOpen ⁡ 𝔼 hil ⁡ n
15 chmph class ≃
16 14 15 cec class TopOpen ⁡ 𝔼 hil ⁡ n ≃
17 16 clly class Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃
18 6 17 wcel wff j ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃
19 8 10 18 w3a wff j ∈ 2 nd 𝜔 ∧ j ∈ Haus ∧ j ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃
20 5 19 wa wff n ∈ ℕ 0 ∧ j ∈ 2 nd 𝜔 ∧ j ∈ Haus ∧ j ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃
21 20 1 2 copab class n j | n ∈ ℕ 0 ∧ j ∈ 2 nd 𝜔 ∧ j ∈ Haus ∧ j ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃
22 0 21 wceq wff ManTop = n j | n ∈ ℕ 0 ∧ j ∈ 2 nd 𝜔 ∧ j ∈ Haus ∧ j ∈ Locally TopOpen ⁡ 𝔼 hil ⁡ n ≃