This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) }