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 ⊢ X = ⋃ J
Assertion stoig ⊢ J ∈ Top ∧ A ⊆ X → Base ndx A TopSet ⁡ ndx J ↾ 𝑡 A ∈ TopSp

Proof

Step Hyp Ref Expression
1 restuni.1 ⊢ X = ⋃ J
2 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
3 resttopon ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A ∈ TopOn ⁡ A
4 2 3 sylanb ⊢ J ∈ Top ∧ A ⊆ X → J ↾ 𝑡 A ∈ TopOn ⁡ A
5 eqid ⊢ Base ndx A TopSet ⁡ ndx J ↾ 𝑡 A = Base ndx A TopSet ⁡ ndx J ↾ 𝑡 A
6 5 eltpsg ⊢ J ↾ 𝑡 A ∈ TopOn ⁡ A → Base ndx A TopSet ⁡ ndx J ↾ 𝑡 A ∈ TopSp
7 4 6 syl ⊢ J ∈ Top ∧ A ⊆ X → Base ndx A TopSet ⁡ ndx J ↾ 𝑡 A ∈ TopSp