Metamath Proof Explorer

Theorem bastop2

Description: A version of bastop1 that doesn't have B C_ J in the antecedent. (Contributed by NM, 3-Feb-2008)

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

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( ( topGen ` B ) = J -> ( ( topGen ` B ) e. Top <-> J e. Top ) )
2 1 biimparc 
 |-  ( ( J e. Top /\ ( topGen ` B ) = J ) -> ( topGen ` B ) e. Top )
3 tgclb 
 |-  ( B e. TopBases <-> ( topGen ` B ) e. Top )
4 2 3 sylibr 
 |-  ( ( J e. Top /\ ( topGen ` B ) = J ) -> B e. TopBases )
5 bastg 
 |-  ( B e. TopBases -> B C_ ( topGen ` B ) )
6 4 5 syl 
 |-  ( ( J e. Top /\ ( topGen ` B ) = J ) -> B C_ ( topGen ` B ) )
7 simpr 
 |-  ( ( J e. Top /\ ( topGen ` B ) = J ) -> ( topGen ` B ) = J )
8 6 7 sseqtrd 
 |-  ( ( J e. Top /\ ( topGen ` B ) = J ) -> B C_ J )
9 8 ex 
 |-  ( J e. Top -> ( ( topGen ` B ) = J -> B C_ J ) )
10 9 pm4.71rd 
 |-  ( J e. Top -> ( ( topGen ` B ) = J <-> ( B C_ J /\ ( topGen ` B ) = J ) ) )
11 bastop1 
 |-  ( ( J e. Top /\ B C_ J ) -> ( ( topGen ` B ) = J <-> A. x e. J E. y ( y C_ B /\ x = U. y ) ) )
12 11 pm5.32da 
 |-  ( J e. Top -> ( ( B C_ J /\ ( topGen ` B ) = J ) <-> ( B C_ J /\ A. x e. J E. y ( y C_ B /\ x = U. y ) ) ) )
13 10 12 bitrd 
 |-  ( J e. Top -> ( ( topGen ` B ) = J <-> ( B C_ J /\ A. x e. J E. y ( y C_ B /\ x = U. y ) ) ) )