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

Metamath Proof Explorer

Theorem restuni

Description: The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypothesis restuni.1 ⊢ X = ⋃ J
Assertion restuni ⊢ J ∈ Top ∧ A ⊆ X → A = ⋃ J ↾ 𝑡 A

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 toponuni ⊢ J ↾ 𝑡 A ∈ TopOn ⁡ A → A = ⋃ J ↾ 𝑡 A
6 4 5 syl ⊢ J ∈ Top ∧ A ⊆ X → A = ⋃ J ↾ 𝑡 A