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 ( ( 𝐽 ∈ 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 ‘ 𝐴 ) ) ⊆ 𝐽 )