Metamath Proof Explorer

Theorem tgss3

Description: A criterion for determining whether one topology is finer than another. Lemma 2.2 of Munkres p. 80 using abbreviations. (Contributed by NM, 20-Jul-2006) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion tgss3 
|- ( ( B e. V /\ C e. W ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> B C_ ( topGen ` C ) ) )

Proof

Step Hyp Ref Expression
1 bastg 
 |-  ( B e. V -> B C_ ( topGen ` B ) )
2 1 adantr 
 |-  ( ( B e. V /\ C e. W ) -> B C_ ( topGen ` B ) )
3 sstr2 
 |-  ( B C_ ( topGen ` B ) -> ( ( topGen ` B ) C_ ( topGen ` C ) -> B C_ ( topGen ` C ) ) )
4 2 3 syl 
 |-  ( ( B e. V /\ C e. W ) -> ( ( topGen ` B ) C_ ( topGen ` C ) -> B C_ ( topGen ` C ) ) )
5 fvex 
 |-  ( topGen ` C ) e. _V
6 tgss 
 |-  ( ( ( topGen ` C ) e. _V /\ B C_ ( topGen ` C ) ) -> ( topGen ` B ) C_ ( topGen ` ( topGen ` C ) ) )
7 5 6 mpan 
 |-  ( B C_ ( topGen ` C ) -> ( topGen ` B ) C_ ( topGen ` ( topGen ` C ) ) )
8 tgidm 
 |-  ( C e. W -> ( topGen ` ( topGen ` C ) ) = ( topGen ` C ) )
9 8 adantl 
 |-  ( ( B e. V /\ C e. W ) -> ( topGen ` ( topGen ` C ) ) = ( topGen ` C ) )
10 9 sseq2d 
 |-  ( ( B e. V /\ C e. W ) -> ( ( topGen ` B ) C_ ( topGen ` ( topGen ` C ) ) <-> ( topGen ` B ) C_ ( topGen ` C ) ) )
11 7 10 syl5ib 
 |-  ( ( B e. V /\ C e. W ) -> ( B C_ ( topGen ` C ) -> ( topGen ` B ) C_ ( topGen ` C ) ) )
12 4 11 impbid 
 |-  ( ( B e. V /\ C e. W ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> B C_ ( topGen ` C ) ) )