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 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )