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 FfBasBAFAFinxFxA

Proof

Step Hyp Ref Expression
1 fbasne0 FfBasBF
2 n0 FxxF
3 1 2 sylib FfBasBxxF
4 ssv xV
5 4 jctr xFxFxV
6 5 eximi xxFxxFxV
7 df-rex xFxVxxFxV
8 6 7 sylibr xxFxFxV
9 3 8 syl FfBasBxFxV
10 inteq A=A=
11 int0 =V
12 10 11 eqtrdi A=A=V
13 12 sseq2d A=xAxV
14 13 rexbidv A=xFxAxFxV
15 9 14 syl5ibrcom FfBasBA=xFxA
16 15 3ad2ant1 FfBasBAFAFinA=xFxA
17 simpl1 FfBasBAFAFinAFfBasB
18 simpl2 FfBasBAFAFinAAF
19 simpr FfBasBAFAFinAA
20 simpl3 FfBasBAFAFinAAFin
21 elfir FfBasBAFAAFinAfiF
22 17 18 19 20 21 syl13anc FfBasBAFAFinAAfiF
23 fbssfi FfBasBAfiFxFxA
24 17 22 23 syl2anc FfBasBAFAFinAxFxA
25 24 ex FfBasBAFAFinAxFxA
26 16 25 pm2.61dne FfBasBAFAFinxFxA