Users' Mathboxes 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 32998
Description: Define the class of 𝑁-manifold topologies, as second countable Hausdorff topologies locally homeomorphic to a ball of the Euclidean space of dimension 𝑁. (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 32997 . 2 class ManTop
2 vn . . . . . 6 setvar 𝑛
32cv 1540 . . . . 5 class 𝑛
4 cn0 12471 . . . . 5 class β„•0
53, 4wcel 2106 . . . 4 wff 𝑛 ∈ β„•0
6 vj . . . . . . 7 setvar 𝑗
76cv 1540 . . . . . 6 class 𝑗
8 c2ndc 22941 . . . . . 6 class 2ndΟ‰
97, 8wcel 2106 . . . . 5 wff 𝑗 ∈ 2ndΟ‰
10 cha 22811 . . . . . 6 class Haus
117, 10wcel 2106 . . . . 5 wff 𝑗 ∈ Haus
12 cehl 24900 . . . . . . . . . 10 class 𝔼hil
133, 12cfv 6543 . . . . . . . . 9 class (𝔼hilβ€˜π‘›)
14 ctopn 17366 . . . . . . . . 9 class TopOpen
1513, 14cfv 6543 . . . . . . . 8 class (TopOpenβ€˜(𝔼hilβ€˜π‘›))
16 chmph 23257 . . . . . . . 8 class ≃
1715, 16cec 8700 . . . . . . 7 class [(TopOpenβ€˜(𝔼hilβ€˜π‘›))] ≃
1817clly 22967 . . . . . 6 class Locally [(TopOpenβ€˜(𝔼hilβ€˜π‘›))] ≃
197, 18wcel 2106 . . . . 5 wff 𝑗 ∈ Locally [(TopOpenβ€˜(𝔼hilβ€˜π‘›))] ≃
209, 11, 19w3a 1087 . . . 4 wff (𝑗 ∈ 2ndΟ‰ ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpenβ€˜(𝔼hilβ€˜π‘›))] ≃ )
215, 20wa 396 . . 3 wff (𝑛 ∈ β„•0 ∧ (𝑗 ∈ 2ndΟ‰ ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpenβ€˜(𝔼hilβ€˜π‘›))] ≃ ))
2221, 2, 6copab 5210 . 2 class {βŸ¨π‘›, π‘—βŸ© ∣ (𝑛 ∈ β„•0 ∧ (𝑗 ∈ 2ndΟ‰ ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpenβ€˜(𝔼hilβ€˜π‘›))] ≃ ))}
231, 22wceq 1541 1 wff ManTop = {βŸ¨π‘›, π‘—βŸ© ∣ (𝑛 ∈ β„•0 ∧ (𝑗 ∈ 2ndΟ‰ ∧ 𝑗 ∈ Haus ∧ 𝑗 ∈ Locally [(TopOpenβ€˜(𝔼hilβ€˜π‘›))] ≃ ))}
Colors of variables: wff setvar class
This definition is referenced by:  relmntop  32999  ismntoplly  33000
  Copyright terms: Public domain W3C validator