Metamath Proof Explorer

Theorem tgss

Description: Subset relation for generated topologies. (Contributed by NM, 7-May-2007)

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

Proof

Step Hyp Ref Expression
1 ssrin 
 |-  ( B C_ C -> ( B i^i ~P x ) C_ ( C i^i ~P x ) )
2 1 unissd 
 |-  ( B C_ C -> U. ( B i^i ~P x ) C_ U. ( C i^i ~P x ) )
3 sstr2 
 |-  ( x C_ U. ( B i^i ~P x ) -> ( U. ( B i^i ~P x ) C_ U. ( C i^i ~P x ) -> x C_ U. ( C i^i ~P x ) ) )
4 2 3 syl5com 
 |-  ( B C_ C -> ( x C_ U. ( B i^i ~P x ) -> x C_ U. ( C i^i ~P x ) ) )
5 4 adantl 
 |-  ( ( C e. V /\ B C_ C ) -> ( x C_ U. ( B i^i ~P x ) -> x C_ U. ( C i^i ~P x ) ) )
6 ssexg 
 |-  ( ( B C_ C /\ C e. V ) -> B e. _V )
7 6 ancoms 
 |-  ( ( C e. V /\ B C_ C ) -> B e. _V )
8 eltg 
 |-  ( B e. _V -> ( x e. ( topGen ` B ) <-> x C_ U. ( B i^i ~P x ) ) )
9 7 8 syl 
 |-  ( ( C e. V /\ B C_ C ) -> ( x e. ( topGen ` B ) <-> x C_ U. ( B i^i ~P x ) ) )
10 eltg 
 |-  ( C e. V -> ( x e. ( topGen ` C ) <-> x C_ U. ( C i^i ~P x ) ) )
11 10 adantr 
 |-  ( ( C e. V /\ B C_ C ) -> ( x e. ( topGen ` C ) <-> x C_ U. ( C i^i ~P x ) ) )
12 5 9 11 3imtr4d 
 |-  ( ( C e. V /\ B C_ C ) -> ( x e. ( topGen ` B ) -> x e. ( topGen ` C ) ) )
13 12 ssrdv 
 |-  ( ( C e. V /\ B C_ C ) -> ( topGen ` B ) C_ ( topGen ` C ) )