This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgfiss

Description: If a subbase is included into a topology, so is the generated topology. (Contributed by FL, 20-Apr-2012) (Proof shortened by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion tgfiss 
|- ( ( J e. Top /\ A C_ J ) -> ( topGen ` ( fi ` A ) ) C_ J )

Proof

Step Hyp Ref Expression
1 fiss 
 |-  ( ( J e. Top /\ A C_ J ) -> ( fi ` A ) C_ ( fi ` J ) )
2 fitop 
 |-  ( J e. Top -> ( fi ` J ) = J )
3 2 adantr 
 |-  ( ( J e. Top /\ A C_ J ) -> ( fi ` J ) = J )
4 1 3 sseqtrd 
 |-  ( ( J e. Top /\ A C_ J ) -> ( fi ` A ) C_ J )
5 tgss 
 |-  ( ( J e. Top /\ ( fi ` A ) C_ J ) -> ( topGen ` ( fi ` A ) ) C_ ( topGen ` J ) )
6 4 5 syldan 
 |-  ( ( J e. Top /\ A C_ J ) -> ( topGen ` ( fi ` A ) ) C_ ( topGen ` J ) )
7 tgtop 
 |-  ( J e. Top -> ( topGen ` J ) = J )
8 7 adantr 
 |-  ( ( J e. Top /\ A C_ J ) -> ( topGen ` J ) = J )
9 6 8 sseqtrd 
 |-  ( ( J e. Top /\ A C_ J ) -> ( topGen ` ( fi ` A ) ) C_ J )