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 )