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 ) ) )