This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fbssfi

Description: A filter base contains subsets of its finite intersections. (Contributed by Mario Carneiro, 26-Nov-2013) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbssfi 
|- ( ( F e. ( fBas ` X ) /\ A e. ( fi ` F ) ) -> E. x e. F x C_ A )

Proof

Step Hyp Ref Expression
1 dffi2 
 |-  ( F e. ( fBas ` X ) -> ( fi ` F ) = |^| { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } )
2 sseq2 
 |-  ( t = ( u i^i v ) -> ( x C_ t <-> x C_ ( u i^i v ) ) )
3 2 rexbidv 
 |-  ( t = ( u i^i v ) -> ( E. x e. F x C_ t <-> E. x e. F x C_ ( u i^i v ) ) )
4 inss1 
 |-  ( u i^i v ) C_ u
5 simp1r 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> u e. ~P U. F )
6 5 elpwid 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> u C_ U. F )
7 4 6 sstrid 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( u i^i v ) C_ U. F )
8 vex 
 |-  u e. _V
9 8 inex1 
 |-  ( u i^i v ) e. _V
10 9 elpw 
 |-  ( ( u i^i v ) e. ~P U. F <-> ( u i^i v ) C_ U. F )
11 7 10 sylibr 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( u i^i v ) e. ~P U. F )
12 simpl 
 |-  ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) -> F e. ( fBas ` X ) )
13 simpl 
 |-  ( ( y e. F /\ y C_ u ) -> y e. F )
14 simpl 
 |-  ( ( z e. F /\ z C_ v ) -> z e. F )
15 fbasssin 
 |-  ( ( F e. ( fBas ` X ) /\ y e. F /\ z e. F ) -> E. x e. F x C_ ( y i^i z ) )
16 12 13 14 15 syl3an 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> E. x e. F x C_ ( y i^i z ) )
17 ss2in 
 |-  ( ( y C_ u /\ z C_ v ) -> ( y i^i z ) C_ ( u i^i v ) )
18 17 ad2ant2l 
 |-  ( ( ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( y i^i z ) C_ ( u i^i v ) )
19 18 3adant1 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( y i^i z ) C_ ( u i^i v ) )
20 sstr 
 |-  ( ( x C_ ( y i^i z ) /\ ( y i^i z ) C_ ( u i^i v ) ) -> x C_ ( u i^i v ) )
21 20 expcom 
 |-  ( ( y i^i z ) C_ ( u i^i v ) -> ( x C_ ( y i^i z ) -> x C_ ( u i^i v ) ) )
22 19 21 syl 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( x C_ ( y i^i z ) -> x C_ ( u i^i v ) ) )
23 22 reximdv 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( E. x e. F x C_ ( y i^i z ) -> E. x e. F x C_ ( u i^i v ) ) )
24 16 23 mpd 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> E. x e. F x C_ ( u i^i v ) )
25 3 11 24 elrabd 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } )
26 25 3expa 
 |-  ( ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) ) /\ ( z e. F /\ z C_ v ) ) -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } )
27 26 rexlimdvaa 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) ) -> ( E. z e. F z C_ v -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
28 27 ralrimivw 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) ) -> A. v e. ~P U. F ( E. z e. F z C_ v -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
29 sseq2 
 |-  ( t = v -> ( x C_ t <-> x C_ v ) )
30 29 rexbidv 
 |-  ( t = v -> ( E. x e. F x C_ t <-> E. x e. F x C_ v ) )
31 sseq1 
 |-  ( x = z -> ( x C_ v <-> z C_ v ) )
32 31 cbvrexvw 
 |-  ( E. x e. F x C_ v <-> E. z e. F z C_ v )
33 30 32 bitrdi 
 |-  ( t = v -> ( E. x e. F x C_ t <-> E. z e. F z C_ v ) )
34 33 ralrab 
 |-  ( A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } <-> A. v e. ~P U. F ( E. z e. F z C_ v -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
35 28 34 sylibr 
 |-  ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) ) -> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } )
36 35 rexlimdvaa 
 |-  ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) -> ( E. y e. F y C_ u -> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
37 36 ralrimiva 
 |-  ( F e. ( fBas ` X ) -> A. u e. ~P U. F ( E. y e. F y C_ u -> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
38 sseq2 
 |-  ( t = u -> ( x C_ t <-> x C_ u ) )
39 38 rexbidv 
 |-  ( t = u -> ( E. x e. F x C_ t <-> E. x e. F x C_ u ) )
40 sseq1 
 |-  ( x = y -> ( x C_ u <-> y C_ u ) )
41 40 cbvrexvw 
 |-  ( E. x e. F x C_ u <-> E. y e. F y C_ u )
42 39 41 bitrdi 
 |-  ( t = u -> ( E. x e. F x C_ t <-> E. y e. F y C_ u ) )
43 42 ralrab 
 |-  ( A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } <-> A. u e. ~P U. F ( E. y e. F y C_ u -> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
44 37 43 sylibr 
 |-  ( F e. ( fBas ` X ) -> A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } )
45 pwuni 
 |-  F C_ ~P U. F
46 ssid 
 |-  t C_ t
47 sseq1 
 |-  ( x = t -> ( x C_ t <-> t C_ t ) )
48 47 rspcev 
 |-  ( ( t e. F /\ t C_ t ) -> E. x e. F x C_ t )
49 46 48 mpan2 
 |-  ( t e. F -> E. x e. F x C_ t )
50 49 rgen 
 |-  A. t e. F E. x e. F x C_ t
51 ssrab 
 |-  ( F C_ { t e. ~P U. F | E. x e. F x C_ t } <-> ( F C_ ~P U. F /\ A. t e. F E. x e. F x C_ t ) )
52 45 50 51 mpbir2an 
 |-  F C_ { t e. ~P U. F | E. x e. F x C_ t }
53 44 52 jctil 
 |-  ( F e. ( fBas ` X ) -> ( F C_ { t e. ~P U. F | E. x e. F x C_ t } /\ A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
54 uniexg 
 |-  ( F e. ( fBas ` X ) -> U. F e. _V )
55 pwexg 
 |-  ( U. F e. _V -> ~P U. F e. _V )
56 rabexg 
 |-  ( ~P U. F e. _V -> { t e. ~P U. F | E. x e. F x C_ t } e. _V )
57 sseq2 
 |-  ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( F C_ z <-> F C_ { t e. ~P U. F | E. x e. F x C_ t } ) )
58 eleq2 
 |-  ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( ( u i^i v ) e. z <-> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
59 58 raleqbi1dv 
 |-  ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( A. v e. z ( u i^i v ) e. z <-> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
60 59 raleqbi1dv 
 |-  ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( A. u e. z A. v e. z ( u i^i v ) e. z <-> A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) )
61 57 60 anbi12d 
 |-  ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) <-> ( F C_ { t e. ~P U. F | E. x e. F x C_ t } /\ A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) )
62 61 elabg 
 |-  ( { t e. ~P U. F | E. x e. F x C_ t } e. _V -> ( { t e. ~P U. F | E. x e. F x C_ t } e. { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } <-> ( F C_ { t e. ~P U. F | E. x e. F x C_ t } /\ A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) )
63 54 55 56 62 4syl 
 |-  ( F e. ( fBas ` X ) -> ( { t e. ~P U. F | E. x e. F x C_ t } e. { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } <-> ( F C_ { t e. ~P U. F | E. x e. F x C_ t } /\ A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) )
64 53 63 mpbird 
 |-  ( F e. ( fBas ` X ) -> { t e. ~P U. F | E. x e. F x C_ t } e. { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } )
65 intss1 
 |-  ( { t e. ~P U. F | E. x e. F x C_ t } e. { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } -> |^| { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } C_ { t e. ~P U. F | E. x e. F x C_ t } )
66 64 65 syl 
 |-  ( F e. ( fBas ` X ) -> |^| { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } C_ { t e. ~P U. F | E. x e. F x C_ t } )
67 1 66 eqsstrd 
 |-  ( F e. ( fBas ` X ) -> ( fi ` F ) C_ { t e. ~P U. F | E. x e. F x C_ t } )
68 67 sselda 
 |-  ( ( F e. ( fBas ` X ) /\ A e. ( fi ` F ) ) -> A e. { t e. ~P U. F | E. x e. F x C_ t } )
69 sseq2 
 |-  ( t = A -> ( x C_ t <-> x C_ A ) )
70 69 rexbidv 
 |-  ( t = A -> ( E. x e. F x C_ t <-> E. x e. F x C_ A ) )
71 70 elrab 
 |-  ( A e. { t e. ~P U. F | E. x e. F x C_ t } <-> ( A e. ~P U. F /\ E. x e. F x C_ A ) )
72 71 simprbi 
 |-  ( A e. { t e. ~P U. F | E. x e. F x C_ t } -> E. x e. F x C_ A )
73 68 72 syl 
 |-  ( ( F e. ( fBas ` X ) /\ A e. ( fi ` F ) ) -> E. x e. F x C_ A )