Metamath Proof Explorer

Theorem restsn2

Description: The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion restsn2 ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ↾ 𝑡 A = 𝒫 A

Proof

Step Hyp Ref Expression
1 snssi ⊢ A ∈ X → A ⊆ X
2 resttopon ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X → J ↾ 𝑡 A ∈ TopOn ⁡ A
3 1 2 sylan2 ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ↾ 𝑡 A ∈ TopOn ⁡ A
4 topsn ⊢ J ↾ 𝑡 A ∈ TopOn ⁡ A → J ↾ 𝑡 A = 𝒫 A
5 3 4 syl ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ↾ 𝑡 A = 𝒫 A