Theorem restsn

Description: The only subspace topology induced by the topology { (/) } . (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Assertion	restsn	$$⊢A\in V\to \left\{\varnothing \right\}{\upharpoonright }_{𝑡}A=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		sn0top	$$⊢\left\{\varnothing \right\}\in \mathrm{Top}$$
2		elrest	$$⊢\left(\left\{\varnothing \right\}\in \mathrm{Top}\wedge A\in V\right)\to \left(x\in \left(\left\{\varnothing \right\}{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists y\in \left\{\varnothing \right\}x=y\cap A\right)$$
3	1 2	mpan	$$⊢A\in V\to \left(x\in \left(\left\{\varnothing \right\}{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists y\in \left\{\varnothing \right\}x=y\cap A\right)$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5		ineq1	$$⊢y=\varnothing \to y\cap A=\varnothing \cap A$$
6		0in	$$⊢\varnothing \cap A=\varnothing$$
7	5 6	eqtrdi	$$⊢y=\varnothing \to y\cap A=\varnothing$$
8	7	eqeq2d	$$⊢y=\varnothing \to \left(x=y\cap A\leftrightarrow x=\varnothing \right)$$
9	4 8	rexsn	$$⊢\exists y\in \left\{\varnothing \right\}x=y\cap A\leftrightarrow x=\varnothing$$
10		velsn	$$⊢x\in \left\{\varnothing \right\}\leftrightarrow x=\varnothing$$
11	9 10	bitr4i	$$⊢\exists y\in \left\{\varnothing \right\}x=y\cap A\leftrightarrow x\in \left\{\varnothing \right\}$$
12	3 11	bitrdi	$$⊢A\in V\to \left(x\in \left(\left\{\varnothing \right\}{\upharpoonright }_{𝑡}A\right)\leftrightarrow x\in \left\{\varnothing \right\}\right)$$
13	12	eqrdv	$$⊢A\in V\to \left\{\varnothing \right\}{\upharpoonright }_{𝑡}A=\left\{\varnothing \right\}$$