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 e. ( Fil ` X ) -> ( F u. { (/) } ) e. Conn )

Proof

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