Metamath Proof Explorer

Theorem basgen2

Description: Given a topology J , show that a subset B satisfying the third antecedent is a basis for it. Lemma 2.3 of Munkres p. 81. (Contributed by NM, 20-Jul-2006) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion basgen2 
|- ( ( J e. Top /\ B C_ J /\ A. x e. J A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) -> ( topGen ` B ) = J )

Proof

Step Hyp Ref Expression
1 dfss3 
 |-  ( J C_ ( topGen ` B ) <-> A. x e. J x e. ( topGen ` B ) )
2 ssexg 
 |-  ( ( B C_ J /\ J e. Top ) -> B e. _V )
3 2 ancoms 
 |-  ( ( J e. Top /\ B C_ J ) -> B e. _V )
4 eltg2b 
 |-  ( B e. _V -> ( x e. ( topGen ` B ) <-> A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) )
5 3 4 syl 
 |-  ( ( J e. Top /\ B C_ J ) -> ( x e. ( topGen ` B ) <-> A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) )
6 5 ralbidv 
 |-  ( ( J e. Top /\ B C_ J ) -> ( A. x e. J x e. ( topGen ` B ) <-> A. x e. J A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) )
7 1 6 bitrid 
 |-  ( ( J e. Top /\ B C_ J ) -> ( J C_ ( topGen ` B ) <-> A. x e. J A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) )
8 7 biimp3ar 
 |-  ( ( J e. Top /\ B C_ J /\ A. x e. J A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) -> J C_ ( topGen ` B ) )
9 basgen 
 |-  ( ( J e. Top /\ B C_ J /\ J C_ ( topGen ` B ) ) -> ( topGen ` B ) = J )
10 8 9 syld3an3 
 |-  ( ( J e. Top /\ B C_ J /\ A. x e. J A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) -> ( topGen ` B ) = J )