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 )