Metamath Proof Explorer

Theorem resttopon2

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

Ref Expression
Assertion resttopon2 ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → J ↾ 𝑡 A ∈ TopOn ⁡ A ∩ X

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
2 resttop ⊢ J ∈ Top ∧ A ∈ V → J ↾ 𝑡 A ∈ Top
3 1 2 sylan ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → J ↾ 𝑡 A ∈ Top
4 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
5 4 ineq2d ⊢ J ∈ TopOn ⁡ X → A ∩ X = A ∩ ⋃ J
6 5 adantr ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → A ∩ X = A ∩ ⋃ J
7 eqid ⊢ ⋃ J = ⋃ J
8 7 restuni2 ⊢ J ∈ Top ∧ A ∈ V → A ∩ ⋃ J = ⋃ J ↾ 𝑡 A
9 1 8 sylan ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → A ∩ ⋃ J = ⋃ J ↾ 𝑡 A
10 6 9 eqtrd ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → A ∩ X = ⋃ J ↾ 𝑡 A
11 istopon ⊢ J ↾ 𝑡 A ∈ TopOn ⁡ A ∩ X ↔ J ↾ 𝑡 A ∈ Top ∧ A ∩ X = ⋃ J ↾ 𝑡 A
12 3 10 11 sylanbrc ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → J ↾ 𝑡 A ∈ TopOn ⁡ A ∩ X