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 )