Metamath Proof Explorer

Theorem hausflim

Description: A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis flimcf.1 ⊢X=⋃J
Assertion hausflim ⊢J∈Haus↔J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf

Proof

Step Hyp Ref Expression
1 flimcf.1 ⊢X=⋃J
2 haustop ⊢J∈Haus→J∈Top
3 hausflimi ⊢J∈Haus→∃*xx∈JfLimf
4 3 ralrimivw ⊢J∈Haus→∀f∈Fil⁡X∃*xx∈JfLimf
5 2 4 jca ⊢J∈Haus→J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf
6 simpl ⊢J∈Top∧z∈X∧w∈X∧z≠w→J∈Top
7 1 toptopon ⊢J∈Top↔J∈TopOn⁡X
8 6 7 sylib ⊢J∈Top∧z∈X∧w∈X∧z≠w→J∈TopOn⁡X
9 simprll ⊢J∈Top∧z∈X∧w∈X∧z≠w→z∈X
10 9 snssd ⊢J∈Top∧z∈X∧w∈X∧z≠w→z⊆X
11 9 snn0d ⊢J∈Top∧z∈X∧w∈X∧z≠w→z≠∅
12 neifil ⊢J∈TopOn⁡X∧z⊆X∧z≠∅→nei⁡J⁡z∈Fil⁡X
13 8 10 11 12 syl3anc ⊢J∈Top∧z∈X∧w∈X∧z≠w→nei⁡J⁡z∈Fil⁡X
14 filfbas ⊢nei⁡J⁡z∈Fil⁡X→nei⁡J⁡z∈fBas⁡X
15 13 14 syl ⊢J∈Top∧z∈X∧w∈X∧z≠w→nei⁡J⁡z∈fBas⁡X
16 simprlr ⊢J∈Top∧z∈X∧w∈X∧z≠w→w∈X
17 16 snssd ⊢J∈Top∧z∈X∧w∈X∧z≠w→w⊆X
18 16 snn0d ⊢J∈Top∧z∈X∧w∈X∧z≠w→w≠∅
19 neifil ⊢J∈TopOn⁡X∧w⊆X∧w≠∅→nei⁡J⁡w∈Fil⁡X
20 8 17 18 19 syl3anc ⊢J∈Top∧z∈X∧w∈X∧z≠w→nei⁡J⁡w∈Fil⁡X
21 filfbas ⊢nei⁡J⁡w∈Fil⁡X→nei⁡J⁡w∈fBas⁡X
22 20 21 syl ⊢J∈Top∧z∈X∧w∈X∧z≠w→nei⁡J⁡w∈fBas⁡X
23 fbunfip ⊢nei⁡J⁡z∈fBas⁡X∧nei⁡J⁡w∈fBas⁡X→¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w↔∀u∈nei⁡J⁡z∀v∈nei⁡J⁡wu∩v≠∅
24 15 22 23 syl2anc ⊢J∈Top∧z∈X∧w∈X∧z≠w→¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w↔∀u∈nei⁡J⁡z∀v∈nei⁡J⁡wu∩v≠∅
25 1 neisspw ⊢J∈Top→nei⁡J⁡z⊆𝒫X
26 1 neisspw ⊢J∈Top→nei⁡J⁡w⊆𝒫X
27 25 26 unssd ⊢J∈Top→nei⁡J⁡z∪nei⁡J⁡w⊆𝒫X
28 27 adantr ⊢J∈Top∧z∈X∧w∈X∧z≠w→nei⁡J⁡z∪nei⁡J⁡w⊆𝒫X
29 28 a1d ⊢J∈Top∧z∈X∧w∈X∧z≠w→¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w→nei⁡J⁡z∪nei⁡J⁡w⊆𝒫X
30 ssun1 ⊢nei⁡J⁡z⊆nei⁡J⁡z∪nei⁡J⁡w
31 filn0 ⊢nei⁡J⁡z∈Fil⁡X→nei⁡J⁡z≠∅
32 13 31 syl ⊢J∈Top∧z∈X∧w∈X∧z≠w→nei⁡J⁡z≠∅
33 ssn0 ⊢nei⁡J⁡z⊆nei⁡J⁡z∪nei⁡J⁡w∧nei⁡J⁡z≠∅→nei⁡J⁡z∪nei⁡J⁡w≠∅
34 30 32 33 sylancr ⊢J∈Top∧z∈X∧w∈X∧z≠w→nei⁡J⁡z∪nei⁡J⁡w≠∅
35 34 a1d ⊢J∈Top∧z∈X∧w∈X∧z≠w→¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w→nei⁡J⁡z∪nei⁡J⁡w≠∅
36 idd ⊢J∈Top∧z∈X∧w∈X∧z≠w→¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w→¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w
37 29 35 36 3jcad ⊢J∈Top∧z∈X∧w∈X∧z≠w→¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w→nei⁡J⁡z∪nei⁡J⁡w⊆𝒫X∧nei⁡J⁡z∪nei⁡J⁡w≠∅∧¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w
38 1 topopn ⊢J∈Top→X∈J
39 38 adantr ⊢J∈Top∧z∈X∧w∈X∧z≠w→X∈J
40 fsubbas ⊢X∈J→fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X↔nei⁡J⁡z∪nei⁡J⁡w⊆𝒫X∧nei⁡J⁡z∪nei⁡J⁡w≠∅∧¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w
41 39 40 syl ⊢J∈Top∧z∈X∧w∈X∧z≠w→fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X↔nei⁡J⁡z∪nei⁡J⁡w⊆𝒫X∧nei⁡J⁡z∪nei⁡J⁡w≠∅∧¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w
42 fgcl ⊢fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∈Fil⁡X
43 42 adantl ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∈Fil⁡X
44 simplrr ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→z≠w
45 9 adantr ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→z∈X
46 16 adantr ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→w∈X
47 fvex ⊢nei⁡J⁡z∈V
48 fvex ⊢nei⁡J⁡w∈V
49 47 48 unex ⊢nei⁡J⁡z∪nei⁡J⁡w∈V
50 ssfii ⊢nei⁡J⁡z∪nei⁡J⁡w∈V→nei⁡J⁡z∪nei⁡J⁡w⊆fi⁡nei⁡J⁡z∪nei⁡J⁡w
51 49 50 ax-mp ⊢nei⁡J⁡z∪nei⁡J⁡w⊆fi⁡nei⁡J⁡z∪nei⁡J⁡w
52 ssfg ⊢fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→fi⁡nei⁡J⁡z∪nei⁡J⁡w⊆XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
53 52 adantl ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→fi⁡nei⁡J⁡z∪nei⁡J⁡w⊆XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
54 51 53 sstrid ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→nei⁡J⁡z∪nei⁡J⁡w⊆XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
55 30 54 sstrid ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→nei⁡J⁡z⊆XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
56 8 adantr ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→J∈TopOn⁡X
57 elflim ⊢J∈TopOn⁡X∧XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∈Fil⁡X→z∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w↔z∈X∧nei⁡J⁡z⊆XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
58 56 43 57 syl2anc ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→z∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w↔z∈X∧nei⁡J⁡z⊆XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
59 45 55 58 mpbir2and ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→z∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
60 54 unssbd ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→nei⁡J⁡w⊆XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
61 elflim ⊢J∈TopOn⁡X∧XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∈Fil⁡X→w∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w↔w∈X∧nei⁡J⁡w⊆XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
62 56 43 61 syl2anc ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→w∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w↔w∈X∧nei⁡J⁡w⊆XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
63 46 60 62 mpbir2and ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→w∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
64 eleq1w ⊢x=z→x∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w↔z∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
65 eleq1w ⊢x=w→x∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w↔w∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
66 64 65 moi ⊢z∈X∧w∈X∧∃*xx∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∧z∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∧w∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→z=w
67 66 3com23 ⊢z∈X∧w∈X∧z∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∧w∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∧∃*xx∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→z=w
68 67 3expia ⊢z∈X∧w∈X∧z∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∧w∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→∃*xx∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→z=w
69 45 46 59 63 68 syl22anc ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→∃*xx∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→z=w
70 69 necon3ad ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→z≠w→¬∃*xx∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
71 44 70 mpd ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→¬∃*xx∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
72 oveq2 ⊢f=XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→JfLimf=JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
73 72 eleq2d ⊢f=XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→x∈JfLimf↔x∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
74 73 mobidv ⊢f=XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→∃*xx∈JfLimf↔∃*xx∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
75 74 notbid ⊢f=XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→¬∃*xx∈JfLimf↔¬∃*xx∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w
76 75 rspcev ⊢XfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w∈Fil⁡X∧¬∃*xx∈JfLimXfilGenfi⁡nei⁡J⁡z∪nei⁡J⁡w→∃f∈Fil⁡X¬∃*xx∈JfLimf
77 43 71 76 syl2anc ⊢J∈Top∧z∈X∧w∈X∧z≠w∧fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→∃f∈Fil⁡X¬∃*xx∈JfLimf
78 77 ex ⊢J∈Top∧z∈X∧w∈X∧z≠w→fi⁡nei⁡J⁡z∪nei⁡J⁡w∈fBas⁡X→∃f∈Fil⁡X¬∃*xx∈JfLimf
79 41 78 sylbird ⊢J∈Top∧z∈X∧w∈X∧z≠w→nei⁡J⁡z∪nei⁡J⁡w⊆𝒫X∧nei⁡J⁡z∪nei⁡J⁡w≠∅∧¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w→∃f∈Fil⁡X¬∃*xx∈JfLimf
80 37 79 syld ⊢J∈Top∧z∈X∧w∈X∧z≠w→¬∅∈fi⁡nei⁡J⁡z∪nei⁡J⁡w→∃f∈Fil⁡X¬∃*xx∈JfLimf
81 24 80 sylbird ⊢J∈Top∧z∈X∧w∈X∧z≠w→∀u∈nei⁡J⁡z∀v∈nei⁡J⁡wu∩v≠∅→∃f∈Fil⁡X¬∃*xx∈JfLimf
82 df-ne ⊢u∩v≠∅↔¬u∩v=∅
83 82 ralbii ⊢∀v∈nei⁡J⁡wu∩v≠∅↔∀v∈nei⁡J⁡w¬u∩v=∅
84 ralnex ⊢∀v∈nei⁡J⁡w¬u∩v=∅↔¬∃v∈nei⁡J⁡wu∩v=∅
85 83 84 bitri ⊢∀v∈nei⁡J⁡wu∩v≠∅↔¬∃v∈nei⁡J⁡wu∩v=∅
86 85 ralbii ⊢∀u∈nei⁡J⁡z∀v∈nei⁡J⁡wu∩v≠∅↔∀u∈nei⁡J⁡z¬∃v∈nei⁡J⁡wu∩v=∅
87 ralnex ⊢∀u∈nei⁡J⁡z¬∃v∈nei⁡J⁡wu∩v=∅↔¬∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅
88 86 87 bitri ⊢∀u∈nei⁡J⁡z∀v∈nei⁡J⁡wu∩v≠∅↔¬∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅
89 rexnal ⊢∃f∈Fil⁡X¬∃*xx∈JfLimf↔¬∀f∈Fil⁡X∃*xx∈JfLimf
90 81 88 89 3imtr3g ⊢J∈Top∧z∈X∧w∈X∧z≠w→¬∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅→¬∀f∈Fil⁡X∃*xx∈JfLimf
91 90 con4d ⊢J∈Top∧z∈X∧w∈X∧z≠w→∀f∈Fil⁡X∃*xx∈JfLimf→∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅
92 91 imp ⊢J∈Top∧z∈X∧w∈X∧z≠w∧∀f∈Fil⁡X∃*xx∈JfLimf→∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅
93 92 an32s ⊢J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf∧z∈X∧w∈X∧z≠w→∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅
94 93 expr ⊢J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf∧z∈X∧w∈X→z≠w→∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅
95 94 ralrimivva ⊢J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf→∀z∈X∀w∈Xz≠w→∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅
96 simpl ⊢J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf→J∈Top
97 96 7 sylib ⊢J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf→J∈TopOn⁡X
98 hausnei2 ⊢J∈TopOn⁡X→J∈Haus↔∀z∈X∀w∈Xz≠w→∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅
99 97 98 syl ⊢J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf→J∈Haus↔∀z∈X∀w∈Xz≠w→∃u∈nei⁡J⁡z∃v∈nei⁡J⁡wu∩v=∅
100 95 99 mpbird ⊢J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf→J∈Haus
101 5 100 impbii ⊢J∈Haus↔J∈Top∧∀f∈Fil⁡X∃*xx∈JfLimf