This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem stoig

Description: The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009) (Proof shortened by Mario Carneiro, 1-May-2015)

Ref Expression
Hypothesis restuni.1 ⊢ 𝑋 = ∪ 𝐽
Assertion stoig ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↾t 𝐴 ) ⟩ } ∈ TopSp )

Proof

Step Hyp Ref Expression
1 restuni.1 ⊢ 𝑋 = ∪ 𝐽
2 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
4 2 3 sylanb ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
5 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↾t 𝐴 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↾t 𝐴 ) ⟩ }
6 5 eltpsg ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) → { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↾t 𝐴 ) ⟩ } ∈ TopSp )
7 4 6 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ↾t 𝐴 ) ⟩ } ∈ TopSp )