This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fbasssin

Description: A filter base contains subsets of its pairwise intersections. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Jeff Hankins, 1-Dec-2010)

Ref Expression
Assertion fbasssin 
|- ( ( F e. ( fBas ` X ) /\ A e. F /\ B e. F ) -> E. x e. F x C_ ( A i^i B ) )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( F e. ( fBas ` X ) -> X e. dom fBas )
2 isfbas2 
 |-  ( X e. dom fBas -> ( F e. ( fBas ` X ) <-> ( F C_ ~P X /\ ( F =/= (/) /\ (/) e/ F /\ A. y e. F A. z e. F E. x e. F x C_ ( y i^i z ) ) ) ) )
3 1 2 syl 
 |-  ( F e. ( fBas ` X ) -> ( F e. ( fBas ` X ) <-> ( F C_ ~P X /\ ( F =/= (/) /\ (/) e/ F /\ A. y e. F A. z e. F E. x e. F x C_ ( y i^i z ) ) ) ) )
4 3 ibi 
 |-  ( F e. ( fBas ` X ) -> ( F C_ ~P X /\ ( F =/= (/) /\ (/) e/ F /\ A. y e. F A. z e. F E. x e. F x C_ ( y i^i z ) ) ) )
5 4 simprd 
 |-  ( F e. ( fBas ` X ) -> ( F =/= (/) /\ (/) e/ F /\ A. y e. F A. z e. F E. x e. F x C_ ( y i^i z ) ) )
6 5 simp3d 
 |-  ( F e. ( fBas ` X ) -> A. y e. F A. z e. F E. x e. F x C_ ( y i^i z ) )
7 ineq1 
 |-  ( y = A -> ( y i^i z ) = ( A i^i z ) )
8 7 sseq2d 
 |-  ( y = A -> ( x C_ ( y i^i z ) <-> x C_ ( A i^i z ) ) )
9 8 rexbidv 
 |-  ( y = A -> ( E. x e. F x C_ ( y i^i z ) <-> E. x e. F x C_ ( A i^i z ) ) )
10 ineq2 
 |-  ( z = B -> ( A i^i z ) = ( A i^i B ) )
11 10 sseq2d 
 |-  ( z = B -> ( x C_ ( A i^i z ) <-> x C_ ( A i^i B ) ) )
12 11 rexbidv 
 |-  ( z = B -> ( E. x e. F x C_ ( A i^i z ) <-> E. x e. F x C_ ( A i^i B ) ) )
13 9 12 rspc2v 
 |-  ( ( A e. F /\ B e. F ) -> ( A. y e. F A. z e. F E. x e. F x C_ ( y i^i z ) -> E. x e. F x C_ ( A i^i B ) ) )
14 6 13 syl5com 
 |-  ( F e. ( fBas ` X ) -> ( ( A e. F /\ B e. F ) -> E. x e. F x C_ ( A i^i B ) ) )
15 14 3impib 
 |-  ( ( F e. ( fBas ` X ) /\ A e. F /\ B e. F ) -> E. x e. F x C_ ( A i^i B ) )