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 ⊆ ∅ ↔ ∃ y y ∈ 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 ∪ ∅ → ∃ y y ∈ x ∧ ¬ y ∈ ∅ → ⋃ x ∈ F ∪ ∅
31 5 30 syl5bi ⊢ 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 → ∀ x x ⊆ 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 ∈ F x ∩ 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 ∈ F x ∩ 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 ↔ ∀ x x ⊆ F ∪ ∅ → ⋃ x ∈ F ∪ ∅ ∧ ∀ x ∈ F ∪ ∅ ∀ y ∈ F ∪ ∅ x ∩ y ∈ F ∪ ∅
71 69 70 syl ⊢ F ∈ Fil ⁡ ⋃ F → F ∪ ∅ ∈ Top ↔ ∀ x x ⊆ 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 syl5bi ⊢ 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