Metamath Proof Explorer


Theorem fbssint

Description: A filter base contains subsets of its finite intersections. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbssint F fBas B A F A Fin x F x A

Proof

Step Hyp Ref Expression
1 fbasne0 F fBas B F
2 n0 F x x F
3 1 2 sylib F fBas B x x F
4 ssv x V
5 4 jctr x F x F x V
6 5 eximi x x F x x F x V
7 df-rex x F x V x x F x V
8 6 7 sylibr x x F x F x V
9 3 8 syl F fBas B x F x V
10 inteq A = A =
11 int0 = V
12 10 11 eqtrdi A = A = V
13 12 sseq2d A = x A x V
14 13 rexbidv A = x F x A x F x V
15 9 14 syl5ibrcom F fBas B A = x F x A
16 15 3ad2ant1 F fBas B A F A Fin A = x F x A
17 simpl1 F fBas B A F A Fin A F fBas B
18 simpl2 F fBas B A F A Fin A A F
19 simpr F fBas B A F A Fin A A
20 simpl3 F fBas B A F A Fin A A Fin
21 elfir F fBas B A F A A Fin A fi F
22 17 18 19 20 21 syl13anc F fBas B A F A Fin A A fi F
23 fbssfi F fBas B A fi F x F x A
24 17 22 23 syl2anc F fBas B A F A Fin A x F x A
25 24 ex F fBas B A F A Fin A x F x A
26 16 25 pm2.61dne F fBas B A F A Fin x F x A