Metamath Proof Explorer

Theorem filconn

Description: A filter gives rise to a connected topology. (Contributed by Jeff Hankins, 6-Dec-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion filconn ⊢F∈Fil⁡X→F∪∅∈Conn

Proof

Step Hyp Ref Expression
1 id ⊢F∈Fil⁡X→F∈Fil⁡X
2 filunibas ⊢F∈Fil⁡X→⋃F=X
3 2 fveq2d ⊢F∈Fil⁡X→Fil⁡⋃F=Fil⁡X
4 1 3 eleqtrrd ⊢F∈Fil⁡X→F∈Fil⁡⋃F
5 nss ⊢¬x⊆∅↔∃yy∈x∧¬y∈∅
6 simpll ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x∧¬y∈∅→F∈Fil⁡⋃F
7 ssel2 ⊢x⊆F∪∅∧y∈x→y∈F∪∅
8 7 adantll ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x→y∈F∪∅
9 elun ⊢y∈F∪∅↔y∈F∨y∈∅
10 8 9 sylib ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x→y∈F∨y∈∅
11 10 orcomd ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x→y∈∅∨y∈F
12 11 ord ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x→¬y∈∅→y∈F
13 12 impr ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x∧¬y∈∅→y∈F
14 uniss ⊢x⊆F∪∅→⋃x⊆⋃F∪∅
15 14 ad2antlr ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x∧¬y∈∅→⋃x⊆⋃F∪∅
16 uniun ⊢⋃F∪∅=⋃F∪⋃∅
17 0ex ⊢∅∈V
18 17 unisn ⊢⋃∅=∅
19 18 uneq2i ⊢⋃F∪⋃∅=⋃F∪∅
20 un0 ⊢⋃F∪∅=⋃F
21 16 19 20 3eqtrri ⊢⋃F=⋃F∪∅
22 15 21 sseqtrrdi ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x∧¬y∈∅→⋃x⊆⋃F
23 elssuni ⊢y∈x→y⊆⋃x
24 23 ad2antrl ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x∧¬y∈∅→y⊆⋃x
25 filss ⊢F∈Fil⁡⋃F∧y∈F∧⋃x⊆⋃F∧y⊆⋃x→⋃x∈F
26 6 13 22 24 25 syl13anc ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x∧¬y∈∅→⋃x∈F
27 elun1 ⊢⋃x∈F→⋃x∈F∪∅
28 26 27 syl ⊢F∈Fil⁡⋃F∧x⊆F∪∅∧y∈x∧¬y∈∅→⋃x∈F∪∅
29 28 ex ⊢F∈Fil⁡⋃F∧x⊆F∪∅→y∈x∧¬y∈∅→⋃x∈F∪∅
30 29 exlimdv ⊢F∈Fil⁡⋃F∧x⊆F∪∅→∃yy∈x∧¬y∈∅→⋃x∈F∪∅
31 5 30 biimtrid ⊢F∈Fil⁡⋃F∧x⊆F∪∅→¬x⊆∅→⋃x∈F∪∅
32 uni0b ⊢⋃x=∅↔x⊆∅
33 ssun2 ⊢∅⊆F∪∅
34 17 snid ⊢∅∈∅
35 33 34 sselii ⊢∅∈F∪∅
36 eleq1 ⊢⋃x=∅→⋃x∈F∪∅↔∅∈F∪∅
37 35 36 mpbiri ⊢⋃x=∅→⋃x∈F∪∅
38 32 37 sylbir ⊢x⊆∅→⋃x∈F∪∅
39 31 38 pm2.61d2 ⊢F∈Fil⁡⋃F∧x⊆F∪∅→⋃x∈F∪∅
40 39 ex ⊢F∈Fil⁡⋃F→x⊆F∪∅→⋃x∈F∪∅
41 40 alrimiv ⊢F∈Fil⁡⋃F→∀xx⊆F∪∅→⋃x∈F∪∅
42 filin ⊢F∈Fil⁡⋃F∧x∈F∧y∈F→x∩y∈F
43 elun1 ⊢x∩y∈F→x∩y∈F∪∅
44 42 43 syl ⊢F∈Fil⁡⋃F∧x∈F∧y∈F→x∩y∈F∪∅
45 44 3expa ⊢F∈Fil⁡⋃F∧x∈F∧y∈F→x∩y∈F∪∅
46 45 ralrimiva ⊢F∈Fil⁡⋃F∧x∈F→∀y∈Fx∩y∈F∪∅
47 elsni ⊢y∈∅→y=∅
48 ineq2 ⊢y=∅→x∩y=x∩∅
49 in0 ⊢x∩∅=∅
50 48 49 eqtrdi ⊢y=∅→x∩y=∅
51 50 35 eqeltrdi ⊢y=∅→x∩y∈F∪∅
52 47 51 syl ⊢y∈∅→x∩y∈F∪∅
53 52 rgen ⊢∀y∈∅x∩y∈F∪∅
54 ralun ⊢∀y∈Fx∩y∈F∪∅∧∀y∈∅x∩y∈F∪∅→∀y∈F∪∅x∩y∈F∪∅
55 46 53 54 sylancl ⊢F∈Fil⁡⋃F∧x∈F→∀y∈F∪∅x∩y∈F∪∅
56 55 ralrimiva ⊢F∈Fil⁡⋃F→∀x∈F∀y∈F∪∅x∩y∈F∪∅
57 elsni ⊢x∈∅→x=∅
58 ineq1 ⊢x=∅→x∩y=∅∩y
59 0in ⊢∅∩y=∅
60 58 59 eqtrdi ⊢x=∅→x∩y=∅
61 60 35 eqeltrdi ⊢x=∅→x∩y∈F∪∅
62 61 ralrimivw ⊢x=∅→∀y∈F∪∅x∩y∈F∪∅
63 57 62 syl ⊢x∈∅→∀y∈F∪∅x∩y∈F∪∅
64 63 rgen ⊢∀x∈∅∀y∈F∪∅x∩y∈F∪∅
65 ralun ⊢∀x∈F∀y∈F∪∅x∩y∈F∪∅∧∀x∈∅∀y∈F∪∅x∩y∈F∪∅→∀x∈F∪∅∀y∈F∪∅x∩y∈F∪∅
66 56 64 65 sylancl ⊢F∈Fil⁡⋃F→∀x∈F∪∅∀y∈F∪∅x∩y∈F∪∅
67 p0ex ⊢∅∈V
68 unexg ⊢F∈Fil⁡⋃F∧∅∈V→F∪∅∈V
69 67 68 mpan2 ⊢F∈Fil⁡⋃F→F∪∅∈V
70 istopg ⊢F∪∅∈V→F∪∅∈Top↔∀xx⊆F∪∅→⋃x∈F∪∅∧∀x∈F∪∅∀y∈F∪∅x∩y∈F∪∅
71 69 70 syl ⊢F∈Fil⁡⋃F→F∪∅∈Top↔∀xx⊆F∪∅→⋃x∈F∪∅∧∀x∈F∪∅∀y∈F∪∅x∩y∈F∪∅
72 41 66 71 mpbir2and ⊢F∈Fil⁡⋃F→F∪∅∈Top
73 21 cldopn ⊢x∈Clsd⁡F∪∅→⋃F∖x∈F∪∅
74 elun ⊢⋃F∖x∈F∪∅↔⋃F∖x∈F∨⋃F∖x∈∅
75 73 74 sylib ⊢x∈Clsd⁡F∪∅→⋃F∖x∈F∨⋃F∖x∈∅
76 elun ⊢x∈F∪∅↔x∈F∨x∈∅
77 filfbas ⊢F∈Fil⁡⋃F→F∈fBas⁡⋃F
78 fbncp ⊢F∈fBas⁡⋃F∧x∈F→¬⋃F∖x∈F
79 77 78 sylan ⊢F∈Fil⁡⋃F∧x∈F→¬⋃F∖x∈F
80 79 pm2.21d ⊢F∈Fil⁡⋃F∧x∈F→⋃F∖x∈F→x=∅
81 80 ex ⊢F∈Fil⁡⋃F→x∈F→⋃F∖x∈F→x=∅
82 57 a1i13 ⊢F∈Fil⁡⋃F→x∈∅→⋃F∖x∈F→x=∅
83 81 82 jaod ⊢F∈Fil⁡⋃F→x∈F∨x∈∅→⋃F∖x∈F→x=∅
84 76 83 biimtrid ⊢F∈Fil⁡⋃F→x∈F∪∅→⋃F∖x∈F→x=∅
85 84 imp ⊢F∈Fil⁡⋃F∧x∈F∪∅→⋃F∖x∈F→x=∅
86 elsni ⊢⋃F∖x∈∅→⋃F∖x=∅
87 elssuni ⊢x∈F∪∅→x⊆⋃F∪∅
88 87 21 sseqtrrdi ⊢x∈F∪∅→x⊆⋃F
89 88 adantl ⊢F∈Fil⁡⋃F∧x∈F∪∅→x⊆⋃F
90 ssdif0 ⊢⋃F⊆x↔⋃F∖x=∅
91 90 biimpri ⊢⋃F∖x=∅→⋃F⊆x
92 eqss ⊢x=⋃F↔x⊆⋃F∧⋃F⊆x
93 92 simplbi2 ⊢x⊆⋃F→⋃F⊆x→x=⋃F
94 89 91 93 syl2im ⊢F∈Fil⁡⋃F∧x∈F∪∅→⋃F∖x=∅→x=⋃F
95 86 94 syl5 ⊢F∈Fil⁡⋃F∧x∈F∪∅→⋃F∖x∈∅→x=⋃F
96 85 95 orim12d ⊢F∈Fil⁡⋃F∧x∈F∪∅→⋃F∖x∈F∨⋃F∖x∈∅→x=∅∨x=⋃F
97 75 96 syl5 ⊢F∈Fil⁡⋃F∧x∈F∪∅→x∈Clsd⁡F∪∅→x=∅∨x=⋃F
98 97 expimpd ⊢F∈Fil⁡⋃F→x∈F∪∅∧x∈Clsd⁡F∪∅→x=∅∨x=⋃F
99 elin ⊢x∈F∪∅∩Clsd⁡F∪∅↔x∈F∪∅∧x∈Clsd⁡F∪∅
100 vex ⊢x∈V
101 100 elpr ⊢x∈∅⋃F↔x=∅∨x=⋃F
102 98 99 101 3imtr4g ⊢F∈Fil⁡⋃F→x∈F∪∅∩Clsd⁡F∪∅→x∈∅⋃F
103 102 ssrdv ⊢F∈Fil⁡⋃F→F∪∅∩Clsd⁡F∪∅⊆∅⋃F
104 21 isconn2 ⊢F∪∅∈Conn↔F∪∅∈Top∧F∪∅∩Clsd⁡F∪∅⊆∅⋃F
105 72 103 104 sylanbrc ⊢F∈Fil⁡⋃F→F∪∅∈Conn
106 4 105 syl ⊢F∈Fil⁡X→F∪∅∈Conn