Metamath Proof Explorer


Definition df-haus

Description: Define the class of all Hausdorff (or T_2) 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)

Ref Expression
Assertion df-haus Haus = { 𝑗 ∈ Top ∣ ∀ 𝑥 𝑗𝑦 𝑗 ( 𝑥𝑦 → ∃ 𝑛𝑗𝑚𝑗 ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cha Haus
1 vj 𝑗
2 ctop Top
3 vx 𝑥
4 1 cv 𝑗
5 4 cuni 𝑗
6 vy 𝑦
7 3 cv 𝑥
8 6 cv 𝑦
9 7 8 wne 𝑥𝑦
10 vn 𝑛
11 vm 𝑚
12 10 cv 𝑛
13 7 12 wcel 𝑥𝑛
14 11 cv 𝑚
15 8 14 wcel 𝑦𝑚
16 12 14 cin ( 𝑛𝑚 )
17 c0
18 16 17 wceq ( 𝑛𝑚 ) = ∅
19 13 15 18 w3a ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ )
20 19 11 4 wrex 𝑚𝑗 ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ )
21 20 10 4 wrex 𝑛𝑗𝑚𝑗 ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ )
22 9 21 wi ( 𝑥𝑦 → ∃ 𝑛𝑗𝑚𝑗 ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ ) )
23 22 6 5 wral 𝑦 𝑗 ( 𝑥𝑦 → ∃ 𝑛𝑗𝑚𝑗 ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ ) )
24 23 3 5 wral 𝑥 𝑗𝑦 𝑗 ( 𝑥𝑦 → ∃ 𝑛𝑗𝑚𝑗 ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ ) )
25 24 1 2 crab { 𝑗 ∈ Top ∣ ∀ 𝑥 𝑗𝑦 𝑗 ( 𝑥𝑦 → ∃ 𝑛𝑗𝑚𝑗 ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ ) ) }
26 0 25 wceq Haus = { 𝑗 ∈ Top ∣ ∀ 𝑥 𝑗𝑦 𝑗 ( 𝑥𝑦 → ∃ 𝑛𝑗𝑚𝑗 ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ ) ) }