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

Definition df-haus 21853
Description: Define the class of all Hausdorff (or T2) 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 21846 . 2 class Haus
2 vx . . . . . . . 8 setvar 𝑥
32cv 1527 . . . . . . 7 class 𝑥
4 vy . . . . . . . 8 setvar 𝑦
54cv 1527 . . . . . . 7 class 𝑦
63, 5wne 3016 . . . . . 6 wff 𝑥𝑦
7 vn . . . . . . . . . 10 setvar 𝑛
82, 7wel 2106 . . . . . . . . 9 wff 𝑥𝑛
9 vm . . . . . . . . . 10 setvar 𝑚
104, 9wel 2106 . . . . . . . . 9 wff 𝑦𝑚
117cv 1527 . . . . . . . . . . 11 class 𝑛
129cv 1527 . . . . . . . . . . 11 class 𝑚
1311, 12cin 3934 . . . . . . . . . 10 class (𝑛𝑚)
14 c0 4290 . . . . . . . . . 10 class
1513, 14wceq 1528 . . . . . . . . 9 wff (𝑛𝑚) = ∅
168, 10, 15w3a 1079 . . . . . . . 8 wff (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅)
17 vj . . . . . . . . 9 setvar 𝑗
1817cv 1527 . . . . . . . 8 class 𝑗
1916, 9, 18wrex 3139 . . . . . . 7 wff 𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅)
2019, 7, 18wrex 3139 . . . . . 6 wff 𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅)
216, 20wi 4 . . . . 5 wff (𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))
2218cuni 4832 . . . . 5 class 𝑗
2321, 4, 22wral 3138 . . . 4 wff 𝑦 𝑗(𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))
2423, 2, 22wral 3138 . . 3 wff 𝑥 𝑗𝑦 𝑗(𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))
25 ctop 21431 . . 3 class Top
2624, 17, 25crab 3142 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗(𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))}
271, 26wceq 1528 1 wff Haus = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗(𝑥𝑦 → ∃𝑛𝑗𝑚𝑗 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))}
Colors of variables: wff setvar class
This definition is referenced by:  ishaus  21860
  Copyright terms: Public domain W3C validator