Metamath Proof Explorer

Theorem 2basgen

Description: Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007) (Revised by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion 2basgen 
|- ( ( B C_ C /\ C C_ ( topGen ` B ) ) -> ( topGen ` B ) = ( topGen ` C ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( topGen ` B ) e. _V
2 1 ssex 
 |-  ( C C_ ( topGen ` B ) -> C e. _V )
3 simpl 
 |-  ( ( B C_ C /\ C C_ ( topGen ` B ) ) -> B C_ C )
4 tgss 
 |-  ( ( C e. _V /\ B C_ C ) -> ( topGen ` B ) C_ ( topGen ` C ) )
5 2 3 4 syl2an2 
 |-  ( ( B C_ C /\ C C_ ( topGen ` B ) ) -> ( topGen ` B ) C_ ( topGen ` C ) )
6 simpr 
 |-  ( ( B C_ C /\ C C_ ( topGen ` B ) ) -> C C_ ( topGen ` B ) )
7 ssexg 
 |-  ( ( B C_ C /\ C e. _V ) -> B e. _V )
8 2 7 sylan2 
 |-  ( ( B C_ C /\ C C_ ( topGen ` B ) ) -> B e. _V )
9 tgss3 
 |-  ( ( C e. _V /\ B e. _V ) -> ( ( topGen ` C ) C_ ( topGen ` B ) <-> C C_ ( topGen ` B ) ) )
10 2 8 9 syl2an2 
 |-  ( ( B C_ C /\ C C_ ( topGen ` B ) ) -> ( ( topGen ` C ) C_ ( topGen ` B ) <-> C C_ ( topGen ` B ) ) )
11 6 10 mpbird 
 |-  ( ( B C_ C /\ C C_ ( topGen ` B ) ) -> ( topGen ` C ) C_ ( topGen ` B ) )
12 5 11 eqssd 
 |-  ( ( B C_ C /\ C C_ ( topGen ` B ) ) -> ( topGen ` B ) = ( topGen ` C ) )