Metamath Proof Explorer

Theorem fgcl

Description: A generated filter is a filter. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fgcl 
|- ( F e. ( fBas ` X ) -> ( X filGen F ) e. ( Fil ` X ) )

Proof

Step Hyp Ref Expression
1 elfg 
 |-  ( F e. ( fBas ` X ) -> ( z e. ( X filGen F ) <-> ( z C_ X /\ E. y e. F y C_ z ) ) )
2 elfvex 
 |-  ( F e. ( fBas ` X ) -> X e. _V )
3 fbasne0 
 |-  ( F e. ( fBas ` X ) -> F =/= (/) )
4 n0 
 |-  ( F =/= (/) <-> E. y y e. F )
5 3 4 sylib 
 |-  ( F e. ( fBas ` X ) -> E. y y e. F )
6 fbelss 
 |-  ( ( F e. ( fBas ` X ) /\ y e. F ) -> y C_ X )
7 6 ex 
 |-  ( F e. ( fBas ` X ) -> ( y e. F -> y C_ X ) )
8 7 ancld 
 |-  ( F e. ( fBas ` X ) -> ( y e. F -> ( y e. F /\ y C_ X ) ) )
9 8 eximdv 
 |-  ( F e. ( fBas ` X ) -> ( E. y y e. F -> E. y ( y e. F /\ y C_ X ) ) )
10 5 9 mpd 
 |-  ( F e. ( fBas ` X ) -> E. y ( y e. F /\ y C_ X ) )
11 df-rex 
 |-  ( E. y e. F y C_ X <-> E. y ( y e. F /\ y C_ X ) )
12 10 11 sylibr 
 |-  ( F e. ( fBas ` X ) -> E. y e. F y C_ X )
13 elfvdm 
 |-  ( F e. ( fBas ` X ) -> X e. dom fBas )
14 sseq2 
 |-  ( z = X -> ( y C_ z <-> y C_ X ) )
15 14 rexbidv 
 |-  ( z = X -> ( E. y e. F y C_ z <-> E. y e. F y C_ X ) )
16 15 sbcieg 
 |-  ( X e. dom fBas -> ( [. X / z ]. E. y e. F y C_ z <-> E. y e. F y C_ X ) )
17 13 16 syl 
 |-  ( F e. ( fBas ` X ) -> ( [. X / z ]. E. y e. F y C_ z <-> E. y e. F y C_ X ) )
18 12 17 mpbird 
 |-  ( F e. ( fBas ` X ) -> [. X / z ]. E. y e. F y C_ z )
19 0nelfb 
 |-  ( F e. ( fBas ` X ) -> -. (/) e. F )
20 0ex 
 |-  (/) e. _V
21 sseq2 
 |-  ( z = (/) -> ( y C_ z <-> y C_ (/) ) )
22 21 rexbidv 
 |-  ( z = (/) -> ( E. y e. F y C_ z <-> E. y e. F y C_ (/) ) )
23 20 22 sbcie 
 |-  ( [. (/) / z ]. E. y e. F y C_ z <-> E. y e. F y C_ (/) )
24 ss0 
 |-  ( y C_ (/) -> y = (/) )
25 24 eleq1d 
 |-  ( y C_ (/) -> ( y e. F <-> (/) e. F ) )
26 25 biimpac 
 |-  ( ( y e. F /\ y C_ (/) ) -> (/) e. F )
27 26 rexlimiva 
 |-  ( E. y e. F y C_ (/) -> (/) e. F )
28 23 27 sylbi 
 |-  ( [. (/) / z ]. E. y e. F y C_ z -> (/) e. F )
29 19 28 nsyl 
 |-  ( F e. ( fBas ` X ) -> -. [. (/) / z ]. E. y e. F y C_ z )
30 sstr 
 |-  ( ( y C_ v /\ v C_ u ) -> y C_ u )
31 30 expcom 
 |-  ( v C_ u -> ( y C_ v -> y C_ u ) )
32 31 reximdv 
 |-  ( v C_ u -> ( E. y e. F y C_ v -> E. y e. F y C_ u ) )
33 32 3ad2ant3 
 |-  ( ( F e. ( fBas ` X ) /\ u C_ X /\ v C_ u ) -> ( E. y e. F y C_ v -> E. y e. F y C_ u ) )
34 vex 
 |-  v e. _V
35 sseq2 
 |-  ( z = v -> ( y C_ z <-> y C_ v ) )
36 35 rexbidv 
 |-  ( z = v -> ( E. y e. F y C_ z <-> E. y e. F y C_ v ) )
37 34 36 sbcie 
 |-  ( [. v / z ]. E. y e. F y C_ z <-> E. y e. F y C_ v )
38 vex 
 |-  u e. _V
39 sseq2 
 |-  ( z = u -> ( y C_ z <-> y C_ u ) )
40 39 rexbidv 
 |-  ( z = u -> ( E. y e. F y C_ z <-> E. y e. F y C_ u ) )
41 38 40 sbcie 
 |-  ( [. u / z ]. E. y e. F y C_ z <-> E. y e. F y C_ u )
42 33 37 41 3imtr4g 
 |-  ( ( F e. ( fBas ` X ) /\ u C_ X /\ v C_ u ) -> ( [. v / z ]. E. y e. F y C_ z -> [. u / z ]. E. y e. F y C_ z ) )
43 fbasssin 
 |-  ( ( F e. ( fBas ` X ) /\ z e. F /\ w e. F ) -> E. y e. F y C_ ( z i^i w ) )
44 43 3expib 
 |-  ( F e. ( fBas ` X ) -> ( ( z e. F /\ w e. F ) -> E. y e. F y C_ ( z i^i w ) ) )
45 sstr2 
 |-  ( y C_ ( z i^i w ) -> ( ( z i^i w ) C_ ( u i^i v ) -> y C_ ( u i^i v ) ) )
46 45 com12 
 |-  ( ( z i^i w ) C_ ( u i^i v ) -> ( y C_ ( z i^i w ) -> y C_ ( u i^i v ) ) )
47 46 reximdv 
 |-  ( ( z i^i w ) C_ ( u i^i v ) -> ( E. y e. F y C_ ( z i^i w ) -> E. y e. F y C_ ( u i^i v ) ) )
48 ss2in 
 |-  ( ( z C_ u /\ w C_ v ) -> ( z i^i w ) C_ ( u i^i v ) )
49 47 48 syl11 
 |-  ( E. y e. F y C_ ( z i^i w ) -> ( ( z C_ u /\ w C_ v ) -> E. y e. F y C_ ( u i^i v ) ) )
50 44 49 syl6 
 |-  ( F e. ( fBas ` X ) -> ( ( z e. F /\ w e. F ) -> ( ( z C_ u /\ w C_ v ) -> E. y e. F y C_ ( u i^i v ) ) ) )
51 50 exp5c 
 |-  ( F e. ( fBas ` X ) -> ( z e. F -> ( w e. F -> ( z C_ u -> ( w C_ v -> E. y e. F y C_ ( u i^i v ) ) ) ) ) )
52 51 imp31 
 |-  ( ( ( F e. ( fBas ` X ) /\ z e. F ) /\ w e. F ) -> ( z C_ u -> ( w C_ v -> E. y e. F y C_ ( u i^i v ) ) ) )
53 52 impancom 
 |-  ( ( ( F e. ( fBas ` X ) /\ z e. F ) /\ z C_ u ) -> ( w e. F -> ( w C_ v -> E. y e. F y C_ ( u i^i v ) ) ) )
54 53 rexlimdv 
 |-  ( ( ( F e. ( fBas ` X ) /\ z e. F ) /\ z C_ u ) -> ( E. w e. F w C_ v -> E. y e. F y C_ ( u i^i v ) ) )
55 54 rexlimdva2 
 |-  ( F e. ( fBas ` X ) -> ( E. z e. F z C_ u -> ( E. w e. F w C_ v -> E. y e. F y C_ ( u i^i v ) ) ) )
56 55 impd 
 |-  ( F e. ( fBas ` X ) -> ( ( E. z e. F z C_ u /\ E. w e. F w C_ v ) -> E. y e. F y C_ ( u i^i v ) ) )
57 56 3ad2ant1 
 |-  ( ( F e. ( fBas ` X ) /\ u C_ X /\ v C_ X ) -> ( ( E. z e. F z C_ u /\ E. w e. F w C_ v ) -> E. y e. F y C_ ( u i^i v ) ) )
58 sseq1 
 |-  ( y = z -> ( y C_ u <-> z C_ u ) )
59 58 cbvrexvw 
 |-  ( E. y e. F y C_ u <-> E. z e. F z C_ u )
60 41 59 bitri 
 |-  ( [. u / z ]. E. y e. F y C_ z <-> E. z e. F z C_ u )
61 sseq1 
 |-  ( y = w -> ( y C_ v <-> w C_ v ) )
62 61 cbvrexvw 
 |-  ( E. y e. F y C_ v <-> E. w e. F w C_ v )
63 37 62 bitri 
 |-  ( [. v / z ]. E. y e. F y C_ z <-> E. w e. F w C_ v )
64 60 63 anbi12i 
 |-  ( ( [. u / z ]. E. y e. F y C_ z /\ [. v / z ]. E. y e. F y C_ z ) <-> ( E. z e. F z C_ u /\ E. w e. F w C_ v ) )
65 38 inex1 
 |-  ( u i^i v ) e. _V
66 sseq2 
 |-  ( z = ( u i^i v ) -> ( y C_ z <-> y C_ ( u i^i v ) ) )
67 66 rexbidv 
 |-  ( z = ( u i^i v ) -> ( E. y e. F y C_ z <-> E. y e. F y C_ ( u i^i v ) ) )
68 65 67 sbcie 
 |-  ( [. ( u i^i v ) / z ]. E. y e. F y C_ z <-> E. y e. F y C_ ( u i^i v ) )
69 57 64 68 3imtr4g 
 |-  ( ( F e. ( fBas ` X ) /\ u C_ X /\ v C_ X ) -> ( ( [. u / z ]. E. y e. F y C_ z /\ [. v / z ]. E. y e. F y C_ z ) -> [. ( u i^i v ) / z ]. E. y e. F y C_ z ) )
70 1 2 18 29 42 69 isfild 
 |-  ( F e. ( fBas ` X ) -> ( X filGen F ) e. ( Fil ` X ) )