Theorem fiinbas

Description: If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	fiinbas	|- ( ( B e. C /\ A. x e. B A. y e. B ( x i^i y ) e. B ) -> B e. TopBases )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- ( x i^i y ) C_ ( x i^i y )
2		eleq2	|- ( w = ( x i^i y ) -> ( z e. w <-> z e. ( x i^i y ) ) )
3		sseq1	|- ( w = ( x i^i y ) -> ( w C_ ( x i^i y ) <-> ( x i^i y ) C_ ( x i^i y ) ) )
4	2 3	anbi12d	|- ( w = ( x i^i y ) -> ( ( z e. w /\ w C_ ( x i^i y ) ) <-> ( z e. ( x i^i y ) /\ ( x i^i y ) C_ ( x i^i y ) ) ) )
5	4	rspcev	|- ( ( ( x i^i y ) e. B /\ ( z e. ( x i^i y ) /\ ( x i^i y ) C_ ( x i^i y ) ) ) -> E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
6	1 5	mpanr2	|- ( ( ( x i^i y ) e. B /\ z e. ( x i^i y ) ) -> E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
7	6	ralrimiva	|- ( ( x i^i y ) e. B -> A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) )
8	7	a1i	|- ( B e. C -> ( ( x i^i y ) e. B -> A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )
9	8	ralimdv	|- ( B e. C -> ( A. y e. B ( x i^i y ) e. B -> A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )
10	9	ralimdv	|- ( B e. C -> ( A. x e. B A. y e. B ( x i^i y ) e. B -> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )
11		isbasis2g	|- ( B e. C -> ( B e. TopBases <-> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )
12	10 11	sylibrd	|- ( B e. C -> ( A. x e. B A. y e. B ( x i^i y ) e. B -> B e. TopBases ) )
13	12	imp	|- ( ( B e. C /\ A. x e. B A. y e. B ( x i^i y ) e. B ) -> B e. TopBases )