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