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 syl5bir ( ( 𝑥𝑚𝑚𝑢 ) → ( ( { 𝑦 } ⊆ 𝑛𝑛𝑣 ) → ( ( 𝑢𝑣 ) = ∅ → ( 𝑥𝑚𝑦𝑛 ∧ ( 𝑚𝑛 ) = ∅ ) ) ) )
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 syl5bir ( ( 𝐽 ∈ 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 ‘ 𝐽 ) ‘ { 𝑦 } ) ( 𝑢𝑣 ) = ∅ ) ) )