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 𝐴 ) ) |