Metamath Proof Explorer

Theorem filuni

Description: The union of a nonempty set of filters with a common base and closed under pairwise union is a filter. (Contributed by Mario Carneiro, 28-Nov-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion filuni 
|- ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> U. F e. ( Fil ` X ) )

Proof

Step Hyp Ref Expression
1 eluni2 
 |-  ( x e. U. F <-> E. f e. F x e. f )
2 ssel2 
 |-  ( ( F C_ ( Fil ` X ) /\ f e. F ) -> f e. ( Fil ` X ) )
3 filelss 
 |-  ( ( f e. ( Fil ` X ) /\ x e. f ) -> x C_ X )
4 3 ex 
 |-  ( f e. ( Fil ` X ) -> ( x e. f -> x C_ X ) )
5 2 4 syl 
 |-  ( ( F C_ ( Fil ` X ) /\ f e. F ) -> ( x e. f -> x C_ X ) )
6 5 rexlimdva 
 |-  ( F C_ ( Fil ` X ) -> ( E. f e. F x e. f -> x C_ X ) )
7 6 3ad2ant1 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> ( E. f e. F x e. f -> x C_ X ) )
8 1 7 syl5bi 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> ( x e. U. F -> x C_ X ) )
9 8 pm4.71rd 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> ( x e. U. F <-> ( x C_ X /\ x e. U. F ) ) )
10 ssn0 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) ) -> ( Fil ` X ) =/= (/) )
11 fvprc 
 |-  ( -. X e. _V -> ( Fil ` X ) = (/) )
12 11 necon1ai 
 |-  ( ( Fil ` X ) =/= (/) -> X e. _V )
13 10 12 syl 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) ) -> X e. _V )
14 13 3adant3 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> X e. _V )
15 filtop 
 |-  ( f e. ( Fil ` X ) -> X e. f )
16 2 15 syl 
 |-  ( ( F C_ ( Fil ` X ) /\ f e. F ) -> X e. f )
17 16 a1d 
 |-  ( ( F C_ ( Fil ` X ) /\ f e. F ) -> ( A. g e. F ( f u. g ) e. F -> X e. f ) )
18 17 ralimdva 
 |-  ( F C_ ( Fil ` X ) -> ( A. f e. F A. g e. F ( f u. g ) e. F -> A. f e. F X e. f ) )
19 r19.2z 
 |-  ( ( F =/= (/) /\ A. f e. F X e. f ) -> E. f e. F X e. f )
20 19 ex 
 |-  ( F =/= (/) -> ( A. f e. F X e. f -> E. f e. F X e. f ) )
21 18 20 sylan9 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) ) -> ( A. f e. F A. g e. F ( f u. g ) e. F -> E. f e. F X e. f ) )
22 21 3impia 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> E. f e. F X e. f )
23 eluni2 
 |-  ( X e. U. F <-> E. f e. F X e. f )
24 22 23 sylibr 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> X e. U. F )
25 sbcel1v 
 |-  ( [. X / x ]. x e. U. F <-> X e. U. F )
26 24 25 sylibr 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> [. X / x ]. x e. U. F )
27 0nelfil 
 |-  ( f e. ( Fil ` X ) -> -. (/) e. f )
28 2 27 syl 
 |-  ( ( F C_ ( Fil ` X ) /\ f e. F ) -> -. (/) e. f )
29 28 ralrimiva 
 |-  ( F C_ ( Fil ` X ) -> A. f e. F -. (/) e. f )
30 29 3ad2ant1 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> A. f e. F -. (/) e. f )
31 sbcel1v 
 |-  ( [. (/) / x ]. x e. U. F <-> (/) e. U. F )
32 eluni2 
 |-  ( (/) e. U. F <-> E. f e. F (/) e. f )
33 31 32 bitri 
 |-  ( [. (/) / x ]. x e. U. F <-> E. f e. F (/) e. f )
34 33 notbii 
 |-  ( -. [. (/) / x ]. x e. U. F <-> -. E. f e. F (/) e. f )
35 ralnex 
 |-  ( A. f e. F -. (/) e. f <-> -. E. f e. F (/) e. f )
36 34 35 bitr4i 
 |-  ( -. [. (/) / x ]. x e. U. F <-> A. f e. F -. (/) e. f )
37 30 36 sylibr 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> -. [. (/) / x ]. x e. U. F )
38 simp13 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ y ) -> A. f e. F A. g e. F ( f u. g ) e. F )
39 r19.29 
 |-  ( ( A. f e. F A. g e. F ( f u. g ) e. F /\ E. f e. F x e. f ) -> E. f e. F ( A. g e. F ( f u. g ) e. F /\ x e. f ) )
40 39 ex 
 |-  ( A. f e. F A. g e. F ( f u. g ) e. F -> ( E. f e. F x e. f -> E. f e. F ( A. g e. F ( f u. g ) e. F /\ x e. f ) ) )
41 38 40 syl 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ y ) -> ( E. f e. F x e. f -> E. f e. F ( A. g e. F ( f u. g ) e. F /\ x e. f ) ) )
42 simp1 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> F C_ ( Fil ` X ) )
43 simp1 
 |-  ( ( F C_ ( Fil ` X ) /\ y C_ X /\ x C_ y ) -> F C_ ( Fil ` X ) )
44 simpl 
 |-  ( ( f e. F /\ ( A. g e. F ( f u. g ) e. F /\ x e. f ) ) -> f e. F )
45 43 44 2 syl2an 
 |-  ( ( ( F C_ ( Fil ` X ) /\ y C_ X /\ x C_ y ) /\ ( f e. F /\ ( A. g e. F ( f u. g ) e. F /\ x e. f ) ) ) -> f e. ( Fil ` X ) )
46 simprrr 
 |-  ( ( ( F C_ ( Fil ` X ) /\ y C_ X /\ x C_ y ) /\ ( f e. F /\ ( A. g e. F ( f u. g ) e. F /\ x e. f ) ) ) -> x e. f )
47 simpl2 
 |-  ( ( ( F C_ ( Fil ` X ) /\ y C_ X /\ x C_ y ) /\ ( f e. F /\ ( A. g e. F ( f u. g ) e. F /\ x e. f ) ) ) -> y C_ X )
48 simpl3 
 |-  ( ( ( F C_ ( Fil ` X ) /\ y C_ X /\ x C_ y ) /\ ( f e. F /\ ( A. g e. F ( f u. g ) e. F /\ x e. f ) ) ) -> x C_ y )
49 filss 
 |-  ( ( f e. ( Fil ` X ) /\ ( x e. f /\ y C_ X /\ x C_ y ) ) -> y e. f )
50 45 46 47 48 49 syl13anc 
 |-  ( ( ( F C_ ( Fil ` X ) /\ y C_ X /\ x C_ y ) /\ ( f e. F /\ ( A. g e. F ( f u. g ) e. F /\ x e. f ) ) ) -> y e. f )
51 50 expr 
 |-  ( ( ( F C_ ( Fil ` X ) /\ y C_ X /\ x C_ y ) /\ f e. F ) -> ( ( A. g e. F ( f u. g ) e. F /\ x e. f ) -> y e. f ) )
52 51 reximdva 
 |-  ( ( F C_ ( Fil ` X ) /\ y C_ X /\ x C_ y ) -> ( E. f e. F ( A. g e. F ( f u. g ) e. F /\ x e. f ) -> E. f e. F y e. f ) )
53 42 52 syl3an1 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ y ) -> ( E. f e. F ( A. g e. F ( f u. g ) e. F /\ x e. f ) -> E. f e. F y e. f ) )
54 41 53 syld 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ y ) -> ( E. f e. F x e. f -> E. f e. F y e. f ) )
55 sbcel1v 
 |-  ( [. x / x ]. x e. U. F <-> x e. U. F )
56 55 1 bitri 
 |-  ( [. x / x ]. x e. U. F <-> E. f e. F x e. f )
57 sbcel1v 
 |-  ( [. y / x ]. x e. U. F <-> y e. U. F )
58 eluni2 
 |-  ( y e. U. F <-> E. f e. F y e. f )
59 57 58 bitri 
 |-  ( [. y / x ]. x e. U. F <-> E. f e. F y e. f )
60 54 56 59 3imtr4g 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ y ) -> ( [. x / x ]. x e. U. F -> [. y / x ]. x e. U. F ) )
61 simp13 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ X ) -> A. f e. F A. g e. F ( f u. g ) e. F )
62 r19.29 
 |-  ( ( A. f e. F A. g e. F ( f u. g ) e. F /\ E. f e. F y e. f ) -> E. f e. F ( A. g e. F ( f u. g ) e. F /\ y e. f ) )
63 62 ex 
 |-  ( A. f e. F A. g e. F ( f u. g ) e. F -> ( E. f e. F y e. f -> E. f e. F ( A. g e. F ( f u. g ) e. F /\ y e. f ) ) )
64 61 63 syl 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ X ) -> ( E. f e. F y e. f -> E. f e. F ( A. g e. F ( f u. g ) e. F /\ y e. f ) ) )
65 simp11 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ X ) -> F C_ ( Fil ` X ) )
66 r19.29 
 |-  ( ( A. g e. F ( f u. g ) e. F /\ E. g e. F x e. g ) -> E. g e. F ( ( f u. g ) e. F /\ x e. g ) )
67 66 ex 
 |-  ( A. g e. F ( f u. g ) e. F -> ( E. g e. F x e. g -> E. g e. F ( ( f u. g ) e. F /\ x e. g ) ) )
68 elun1 
 |-  ( y e. f -> y e. ( f u. g ) )
69 elun2 
 |-  ( x e. g -> x e. ( f u. g ) )
70 68 69 anim12i 
 |-  ( ( y e. f /\ x e. g ) -> ( y e. ( f u. g ) /\ x e. ( f u. g ) ) )
71 eleq2 
 |-  ( h = ( f u. g ) -> ( y e. h <-> y e. ( f u. g ) ) )
72 eleq2 
 |-  ( h = ( f u. g ) -> ( x e. h <-> x e. ( f u. g ) ) )
73 71 72 anbi12d 
 |-  ( h = ( f u. g ) -> ( ( y e. h /\ x e. h ) <-> ( y e. ( f u. g ) /\ x e. ( f u. g ) ) ) )
74 73 rspcev 
 |-  ( ( ( f u. g ) e. F /\ ( y e. ( f u. g ) /\ x e. ( f u. g ) ) ) -> E. h e. F ( y e. h /\ x e. h ) )
75 70 74 sylan2 
 |-  ( ( ( f u. g ) e. F /\ ( y e. f /\ x e. g ) ) -> E. h e. F ( y e. h /\ x e. h ) )
76 75 an12s 
 |-  ( ( y e. f /\ ( ( f u. g ) e. F /\ x e. g ) ) -> E. h e. F ( y e. h /\ x e. h ) )
77 76 ex 
 |-  ( y e. f -> ( ( ( f u. g ) e. F /\ x e. g ) -> E. h e. F ( y e. h /\ x e. h ) ) )
78 77 ad2antlr 
 |-  ( ( ( f e. F /\ y e. f ) /\ g e. F ) -> ( ( ( f u. g ) e. F /\ x e. g ) -> E. h e. F ( y e. h /\ x e. h ) ) )
79 78 rexlimdva 
 |-  ( ( f e. F /\ y e. f ) -> ( E. g e. F ( ( f u. g ) e. F /\ x e. g ) -> E. h e. F ( y e. h /\ x e. h ) ) )
80 67 79 syl9r 
 |-  ( ( f e. F /\ y e. f ) -> ( A. g e. F ( f u. g ) e. F -> ( E. g e. F x e. g -> E. h e. F ( y e. h /\ x e. h ) ) ) )
81 80 impr 
 |-  ( ( f e. F /\ ( y e. f /\ A. g e. F ( f u. g ) e. F ) ) -> ( E. g e. F x e. g -> E. h e. F ( y e. h /\ x e. h ) ) )
82 81 ancom2s 
 |-  ( ( f e. F /\ ( A. g e. F ( f u. g ) e. F /\ y e. f ) ) -> ( E. g e. F x e. g -> E. h e. F ( y e. h /\ x e. h ) ) )
83 82 rexlimiva 
 |-  ( E. f e. F ( A. g e. F ( f u. g ) e. F /\ y e. f ) -> ( E. g e. F x e. g -> E. h e. F ( y e. h /\ x e. h ) ) )
84 83 imp 
 |-  ( ( E. f e. F ( A. g e. F ( f u. g ) e. F /\ y e. f ) /\ E. g e. F x e. g ) -> E. h e. F ( y e. h /\ x e. h ) )
85 ssel2 
 |-  ( ( F C_ ( Fil ` X ) /\ h e. F ) -> h e. ( Fil ` X ) )
86 filin 
 |-  ( ( h e. ( Fil ` X ) /\ y e. h /\ x e. h ) -> ( y i^i x ) e. h )
87 86 3expib 
 |-  ( h e. ( Fil ` X ) -> ( ( y e. h /\ x e. h ) -> ( y i^i x ) e. h ) )
88 85 87 syl 
 |-  ( ( F C_ ( Fil ` X ) /\ h e. F ) -> ( ( y e. h /\ x e. h ) -> ( y i^i x ) e. h ) )
89 88 reximdva 
 |-  ( F C_ ( Fil ` X ) -> ( E. h e. F ( y e. h /\ x e. h ) -> E. h e. F ( y i^i x ) e. h ) )
90 65 84 89 syl2im 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ X ) -> ( ( E. f e. F ( A. g e. F ( f u. g ) e. F /\ y e. f ) /\ E. g e. F x e. g ) -> E. h e. F ( y i^i x ) e. h ) )
91 64 90 syland 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ X ) -> ( ( E. f e. F y e. f /\ E. g e. F x e. g ) -> E. h e. F ( y i^i x ) e. h ) )
92 eluni2 
 |-  ( x e. U. F <-> E. g e. F x e. g )
93 55 92 bitri 
 |-  ( [. x / x ]. x e. U. F <-> E. g e. F x e. g )
94 59 93 anbi12i 
 |-  ( ( [. y / x ]. x e. U. F /\ [. x / x ]. x e. U. F ) <-> ( E. f e. F y e. f /\ E. g e. F x e. g ) )
95 sbcel1v 
 |-  ( [. ( y i^i x ) / x ]. x e. U. F <-> ( y i^i x ) e. U. F )
96 eluni2 
 |-  ( ( y i^i x ) e. U. F <-> E. h e. F ( y i^i x ) e. h )
97 95 96 bitri 
 |-  ( [. ( y i^i x ) / x ]. x e. U. F <-> E. h e. F ( y i^i x ) e. h )
98 91 94 97 3imtr4g 
 |-  ( ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) /\ y C_ X /\ x C_ X ) -> ( ( [. y / x ]. x e. U. F /\ [. x / x ]. x e. U. F ) -> [. ( y i^i x ) / x ]. x e. U. F ) )
99 9 14 26 37 60 98 isfild 
 |-  ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> U. F e. ( Fil ` X ) )