Description: The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | restin.1 | ⊢ 𝑋 = ∪ 𝐽 | |
| Assertion | restuni2 | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ 𝑋 ) = ∪ ( 𝐽 ↾t 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | restin.1 | ⊢ 𝑋 = ∪ 𝐽 | |
| 2 | simpl | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → 𝐽 ∈ Top ) | |
| 3 | inss2 | ⊢ ( 𝐴 ∩ 𝑋 ) ⊆ 𝑋 | |
| 4 | 1 | restuni | ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∩ 𝑋 ) ⊆ 𝑋 ) → ( 𝐴 ∩ 𝑋 ) = ∪ ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) ) |
| 5 | 2 3 4 | sylancl | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ 𝑋 ) = ∪ ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) ) |
| 6 | 1 | restin | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) ) |
| 7 | 6 | unieqd | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ∪ ( 𝐽 ↾t 𝐴 ) = ∪ ( 𝐽 ↾t ( 𝐴 ∩ 𝑋 ) ) ) |
| 8 | 5 7 | eqtr4d | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ 𝑋 ) = ∪ ( 𝐽 ↾t 𝐴 ) ) |