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