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 ) )