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 | ⊢ 𝑋 = ∪ 𝐽 | |
| Assertion | restuni | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) ) |
| 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 | toponuni | ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) ) | |
| 6 | 4 5 | syl | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) ) |