# 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 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\in {X}\right)\to {J}{↾}_{𝑡}\left\{{A}\right\}=𝒫\left\{{A}\right\}$

### Proof

Step Hyp Ref Expression
1 snssi ${⊢}{A}\in {X}\to \left\{{A}\right\}\subseteq {X}$
2 resttopon ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \left\{{A}\right\}\subseteq {X}\right)\to {J}{↾}_{𝑡}\left\{{A}\right\}\in \mathrm{TopOn}\left(\left\{{A}\right\}\right)$
3 1 2 sylan2 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\in {X}\right)\to {J}{↾}_{𝑡}\left\{{A}\right\}\in \mathrm{TopOn}\left(\left\{{A}\right\}\right)$
4 topsn ${⊢}{J}{↾}_{𝑡}\left\{{A}\right\}\in \mathrm{TopOn}\left(\left\{{A}\right\}\right)\to {J}{↾}_{𝑡}\left\{{A}\right\}=𝒫\left\{{A}\right\}$
5 3 4 syl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {A}\in {X}\right)\to {J}{↾}_{𝑡}\left\{{A}\right\}=𝒫\left\{{A}\right\}$