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