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

Metamath Proof Explorer

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 )