Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-haus Structured version   Visualization version   GIF version

Definition df-haus 20929
 Description: Define the class of all Hausdorff spaces. A Hausdorff space is a topology in which distinct points have disjoint open neighborhoods. Definition of Hausdorff space in [Munkres] p. 98. (Contributed by NM, 8-Mar-2007.)
Assertion
Ref Expression
df-haus Haus = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗(𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))}
Distinct variable group:   𝑗,𝑚,𝑛,𝑥,𝑦

Detailed syntax breakdown of Definition df-haus
StepHypRef Expression
1 cha 20922 . 2 class Haus
2 vx . . . . . . . 8 setvar 𝑥
32cv 1474 . . . . . . 7 class 𝑥
4 vy . . . . . . . 8 setvar 𝑦
54cv 1474 . . . . . . 7 class 𝑦
63, 5wne 2780 . . . . . 6 wff 𝑥𝑦
7 vn . . . . . . . . . 10 setvar 𝑛
82, 7wel 1978 . . . . . . . . 9 wff 𝑥𝑛
9 vm . . . . . . . . . 10 setvar 𝑚
104, 9wel 1978 . . . . . . . . 9 wff 𝑦𝑚
117cv 1474 . . . . . . . . . . 11 class 𝑛
129cv 1474 . . . . . . . . . . 11 class 𝑚
1311, 12cin 3539 . . . . . . . . . 10 class (𝑛𝑚)
14 c0 3874 . . . . . . . . . 10 class
1513, 14wceq 1475 . . . . . . . . 9 wff (𝑛𝑚) = ∅
168, 10, 15w3a 1031 . . . . . . . 8 wff (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅)
17 vj . . . . . . . . 9 setvar 𝑗
1817cv 1474 . . . . . . . 8 class 𝑗
1916, 9, 18wrex 2897 . . . . . . 7 wff 𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅)
2019, 7, 18wrex 2897 . . . . . 6 wff 𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅)
216, 20wi 4 . . . . 5 wff (𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))
2218cuni 4372 . . . . 5 class 𝑗
2321, 4, 22wral 2896 . . . 4 wff 𝑦 𝑗(𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))
2423, 2, 22wral 2896 . . 3 wff 𝑥 𝑗𝑦 𝑗(𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))
25 ctop 20517 . . 3 class Top
2624, 17, 25crab 2900 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗(𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))}
271, 26wceq 1475 1 wff Haus = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗(𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))}
 Colors of variables: wff setvar class This definition is referenced by:  ishaus  20936
 Copyright terms: Public domain W3C validator