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 )