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

Metamath Proof Explorer

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