Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mntop Structured version   Visualization version   GIF version

Definition df-mntop 30195
 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
StepHypRef Expression
1 cmntop 30194 . 2 class ManTop
2 vn . . . . . 6 setvar 𝑛
32cv 1522 . . . . 5 class 𝑛
4 cn0 11330 . . . . 5 class 0
53, 4wcel 2030 . . . 4 wff 𝑛 ∈ ℕ0
6 vj . . . . . . 7 setvar 𝑗
76cv 1522 . . . . . 6 class 𝑗
8 c2ndc 21289 . . . . . 6 class 2nd𝜔
97, 8wcel 2030 . . . . 5 wff 𝑗 ∈ 2nd𝜔
10 cha 21160 . . . . . 6 class Haus
117, 10wcel 2030 . . . . 5 wff 𝑗 ∈ Haus
12 cehl 23218 . . . . . . . . . 10 class 𝔼hil
133, 12cfv 5926 . . . . . . . . 9 class (𝔼hil𝑛)
14 ctopn 16129 . . . . . . . . 9 class TopOpen
1513, 14cfv 5926 . . . . . . . 8 class (TopOpen‘(𝔼hil𝑛))
16 chmph 21605 . . . . . . . 8 class
1715, 16cec 7785 . . . . . . 7 class [(TopOpen‘(𝔼hil𝑛))] ≃
1817clly 21315 . . . . . 6 class Locally [(TopOpen‘(𝔼hil𝑛))] ≃
197, 18wcel 2030 . . . . 5 wff 𝑗 ∈ Locally [(TopOpen‘(𝔼hil𝑛))] ≃
209, 11, 19w3a 1054 . . . 4 wff (𝑗 ∈ 2nd𝜔 ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil𝑛))] ≃ )
215, 20wa 383 . . 3 wff (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2nd𝜔 ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil𝑛))] ≃ ))
2221, 2, 6copab 4745 . 2 class {⟨𝑛, 𝑗⟩ ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2nd𝜔 ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil𝑛))] ≃ ))}
231, 22wceq 1523 1 wff ManTop = {⟨𝑛, 𝑗⟩ ∣ (𝑛 ∈ ℕ0 ∧ (𝑗 ∈ 2nd𝜔 ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpen‘(𝔼hil𝑛))] ≃ ))}
 Colors of variables: wff setvar class This definition is referenced by:  relmntop  30196  ismntoplly  30197
 Copyright terms: Public domain W3C validator