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

Metamath Proof Explorer

Theorem ishaus

Description: The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007)

Ref Expression
Hypothesis ist0.1 ⊢ 𝑋 = ∪ 𝐽
Assertion ishaus ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ 𝑋 = ∪ 𝐽
2 unieq ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
3 2 1 eqtr4di ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = 𝑋 )
4 rexeq ⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
5 4 rexeqbi1dv ⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
6 5 imbi2d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ↔ ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
7 3 6 raleqbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
8 3 7 raleqbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
9 df-haus ⊢ Haus = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝑗 ∃ 𝑚 ∈ 𝑗 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) }
10 8 9 elrab2 ⊢ ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )