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 )