Theorem hausnei

Description: Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007)

	Ref	Expression
Hypothesis	ist0.1	⊢ 𝑋 = ∪ 𝐽
Assertion	hausnei	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑃 ≠ 𝑄 ) ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		ist0.1	⊢ 𝑋 = ∪ 𝐽
2	1	ishaus	⊢ ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
3	2	simprbi	⊢ ( 𝐽 ∈ Haus → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
4		neeq1	⊢ ( 𝑥 = 𝑃 → ( 𝑥 ≠ 𝑦 ↔ 𝑃 ≠ 𝑦 ) )
5		eleq1	⊢ ( 𝑥 = 𝑃 → ( 𝑥 ∈ 𝑛 ↔ 𝑃 ∈ 𝑛 ) )
6	5	3anbi1d	⊢ ( 𝑥 = 𝑃 → ( ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ( 𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
7	6	2rexbidv	⊢ ( 𝑥 = 𝑃 → ( ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
8	4 7	imbi12d	⊢ ( 𝑥 = 𝑃 → ( ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ↔ ( 𝑃 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
9		neeq2	⊢ ( 𝑦 = 𝑄 → ( 𝑃 ≠ 𝑦 ↔ 𝑃 ≠ 𝑄 ) )
10		eleq1	⊢ ( 𝑦 = 𝑄 → ( 𝑦 ∈ 𝑚 ↔ 𝑄 ∈ 𝑚 ) )
11	10	3anbi2d	⊢ ( 𝑦 = 𝑄 → ( ( 𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ( 𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
12	11	2rexbidv	⊢ ( 𝑦 = 𝑄 → ( ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ↔ ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) )
13	9 12	imbi12d	⊢ ( 𝑦 = 𝑄 → ( ( 𝑃 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ↔ ( 𝑃 ≠ 𝑄 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
14	8 13	rspc2v	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( 𝑃 ≠ 𝑄 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
15	3 14	syl5	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝐽 ∈ Haus → ( 𝑃 ≠ 𝑄 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
16	15	ex	⊢ ( 𝑃 ∈ 𝑋 → ( 𝑄 ∈ 𝑋 → ( 𝐽 ∈ Haus → ( 𝑃 ≠ 𝑄 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) ) )
17	16	com3r	⊢ ( 𝐽 ∈ Haus → ( 𝑃 ∈ 𝑋 → ( 𝑄 ∈ 𝑋 → ( 𝑃 ≠ 𝑄 → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) ) )
18	17	3imp2	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑃 ≠ 𝑄 ) ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) )