Metamath Proof Explorer

Theorem hausnei2

Description: The Hausdorff condition still holds if one considers general neighborhoods instead of open sets. (Contributed by Jeff Hankins, 5-Sep-2009)

Ref Expression
Assertion hausnei2 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Haus ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 ishaus2 ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Haus ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
2 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
3 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → 𝐽 ∈ Top )
4 simp2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → 𝑚 ∈ 𝐽 )
5 simp1 ⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → 𝑥 ∈ 𝑚 )
6 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑥 ∈ 𝑚 ) → 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
7 3 4 5 6 syl2an3an ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) → 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
8 simp3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → 𝑛 ∈ 𝐽 )
9 simp2 ⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → 𝑦 ∈ 𝑛 )
10 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑛 ∈ 𝐽 ∧ 𝑦 ∈ 𝑛 ) → 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
11 3 8 9 10 syl2an3an ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) → 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
12 simpr3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) → ( 𝑚 ∩ 𝑛 ) = ∅ )
13 ineq1 ⊢ ( 𝑢 = 𝑚 → ( 𝑢 ∩ 𝑣 ) = ( 𝑚 ∩ 𝑣 ) )
14 13 eqeq1d ⊢ ( 𝑢 = 𝑚 → ( ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ( 𝑚 ∩ 𝑣 ) = ∅ ) )
15 ineq2 ⊢ ( 𝑣 = 𝑛 → ( 𝑚 ∩ 𝑣 ) = ( 𝑚 ∩ 𝑛 ) )
16 15 eqeq1d ⊢ ( 𝑣 = 𝑛 → ( ( 𝑚 ∩ 𝑣 ) = ∅ ↔ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
17 14 16 rspc2ev ⊢ ( ( 𝑚 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
18 7 11 12 17 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
19 18 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) )
20 19 3expib ⊢ ( 𝐽 ∈ Top → ( ( 𝑚 ∈ 𝐽 ∧ 𝑛 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
21 20 rexlimdvv ⊢ ( 𝐽 ∈ Top → ( ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) )
22 neii2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) )
23 22 ex ⊢ ( 𝐽 ∈ Top → ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) → ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) )
24 neii2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) → ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) )
25 24 ex ⊢ ( 𝐽 ∈ Top → ( 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) → ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) )
26 vex ⊢ 𝑥 ∈ V
27 26 snss ⊢ ( 𝑥 ∈ 𝑚 ↔ { 𝑥 } ⊆ 𝑚 )
28 27 anbi1i ⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ↔ ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) )
29 vex ⊢ 𝑦 ∈ V
30 29 snss ⊢ ( 𝑦 ∈ 𝑛 ↔ { 𝑦 } ⊆ 𝑛 )
31 30 anbi1i ⊢ ( ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ↔ ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) )
32 simp1l ⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → 𝑥 ∈ 𝑚 )
33 simp2l ⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → 𝑦 ∈ 𝑛 )
34 ss2in ⊢ ( ( 𝑚 ⊆ 𝑢 ∧ 𝑛 ⊆ 𝑣 ) → ( 𝑚 ∩ 𝑛 ) ⊆ ( 𝑢 ∩ 𝑣 ) )
35 ssn0 ⊢ ( ( ( 𝑚 ∩ 𝑛 ) ⊆ ( 𝑢 ∩ 𝑣 ) ∧ ( 𝑚 ∩ 𝑛 ) ≠ ∅ ) → ( 𝑢 ∩ 𝑣 ) ≠ ∅ )
36 35 ex ⊢ ( ( 𝑚 ∩ 𝑛 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( ( 𝑚 ∩ 𝑛 ) ≠ ∅ → ( 𝑢 ∩ 𝑣 ) ≠ ∅ ) )
37 36 necon4d ⊢ ( ( 𝑚 ∩ 𝑛 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑚 ∩ 𝑛 ) = ∅ ) )
38 34 37 syl ⊢ ( ( 𝑚 ⊆ 𝑢 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑚 ∩ 𝑛 ) = ∅ ) )
39 38 ad2ant2l ⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑚 ∩ 𝑛 ) = ∅ ) )
40 39 3impia ⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ( 𝑚 ∩ 𝑛 ) = ∅ )
41 32 33 40 3jca ⊢ ( ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) )
42 41 3exp ⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ( 𝑦 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
43 31 42 biimtrrid ⊢ ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
44 43 com3r ⊢ ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
45 44 imp ⊢ ( ( ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) → ( ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
46 45 3adant1 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) → ( ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
47 46 reximdv ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ) → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
48 47 3exp ⊢ ( 𝐽 ∈ Top → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) )
49 48 com34 ⊢ ( 𝐽 ∈ Top → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) )
50 49 3imp ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ( 𝑥 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
51 28 50 biimtrrid ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
52 51 reximdv ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
53 52 3exp ⊢ ( 𝐽 ∈ Top → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) )
54 53 com24 ⊢ ( 𝐽 ∈ Top → ( ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) → ( ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) ) )
55 54 impd ⊢ ( 𝐽 ∈ Top → ( ( ∃ 𝑚 ∈ 𝐽 ( { 𝑥 } ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑢 ) ∧ ∃ 𝑛 ∈ 𝐽 ( { 𝑦 } ⊆ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
56 23 25 55 syl2and ⊢ ( 𝐽 ∈ Top → ( ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ) )
57 56 rexlimdvv ⊢ ( 𝐽 ∈ Top → ( ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) )
58 21 57 impbid ⊢ ( 𝐽 ∈ Top → ( ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ↔ ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) )
59 58 imbi2d ⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
60 59 2ralbidv ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
61 2 60 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑚 ∈ 𝐽 ∃ 𝑛 ∈ 𝐽 ( 𝑥 ∈ 𝑚 ∧ 𝑦 ∈ 𝑛 ∧ ( 𝑚 ∩ 𝑛 ) = ∅ ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
62 1 61 bitrd ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Haus ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≠ 𝑦 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )