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	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ( topGen ‘ ( fi ‘ 𝐴 ) ) ⊆ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		fiss	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ( fi ‘ 𝐴 ) ⊆ ( fi ‘ 𝐽 ) )
2		fitop	⊢ ( 𝐽 ∈ Top → ( fi ‘ 𝐽 ) = 𝐽 )
3	2	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ( fi ‘ 𝐽 ) = 𝐽 )
4	1 3	sseqtrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ( fi ‘ 𝐴 ) ⊆ 𝐽 )
5		tgss	⊢ ( ( 𝐽 ∈ Top ∧ ( fi ‘ 𝐴 ) ⊆ 𝐽 ) → ( topGen ‘ ( fi ‘ 𝐴 ) ) ⊆ ( topGen ‘ 𝐽 ) )
6	4 5	syldan	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ( topGen ‘ ( fi ‘ 𝐴 ) ) ⊆ ( topGen ‘ 𝐽 ) )
7		tgtop	⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
8	7	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ( topGen ‘ 𝐽 ) = 𝐽 )
9	6 8	sseqtrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ) → ( topGen ‘ ( fi ‘ 𝐴 ) ) ⊆ 𝐽 )