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 e. ( fBas ` B ) /\ A C_ F /\ A e. Fin ) -> E. x e. F x C_ |^| A )

Proof

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