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{\upharpoonright }_{𝑡}\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{\upharpoonright }_{𝑡}\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{\upharpoonright }_{𝑡}\left\{A\right\}\in \mathrm{TopOn}\left(\left\{A\right\}\right)$$
4		topsn	$$⊢J{\upharpoonright }_{𝑡}\left\{A\right\}\in \mathrm{TopOn}\left(\left\{A\right\}\right)\to J{\upharpoonright }_{𝑡}\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{\upharpoonright }_{𝑡}\left\{A\right\}=𝒫\left\{A\right\}$$