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 )