Metamath Proof Explorer

Theorem basgen

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 using abbreviations. (Contributed by NM, 22-Jul-2006) (Revised by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion basgen 
|- ( ( J e. Top /\ B C_ J /\ J C_ ( topGen ` B ) ) -> ( topGen ` B ) = J )

Proof

Step Hyp Ref Expression
1 tgss 
 |-  ( ( J e. Top /\ B C_ J ) -> ( topGen ` B ) C_ ( topGen ` J ) )
2 1 3adant3 
 |-  ( ( J e. Top /\ B C_ J /\ J C_ ( topGen ` B ) ) -> ( topGen ` B ) C_ ( topGen ` J ) )
3 tgtop 
 |-  ( J e. Top -> ( topGen ` J ) = J )
4 3 3ad2ant1 
 |-  ( ( J e. Top /\ B C_ J /\ J C_ ( topGen ` B ) ) -> ( topGen ` J ) = J )
5 2 4 sseqtrd 
 |-  ( ( J e. Top /\ B C_ J /\ J C_ ( topGen ` B ) ) -> ( topGen ` B ) C_ J )
6 simp3 
 |-  ( ( J e. Top /\ B C_ J /\ J C_ ( topGen ` B ) ) -> J C_ ( topGen ` B ) )
7 5 6 eqssd 
 |-  ( ( J e. Top /\ B C_ J /\ J C_ ( topGen ` B ) ) -> ( topGen ` B ) = J )