Theorem restsspw

Description: The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	restsspw	$$⊢J{\upharpoonright }_{𝑡}A\subseteq 𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		n0i	$$⊢x\in \left(J{\upharpoonright }_{𝑡}A\right)\to \neg J{\upharpoonright }_{𝑡}A=\varnothing$$
2		restfn	$$⊢{\upharpoonright }_{𝑡}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
3		fndm	$$⊢{\upharpoonright }_{𝑡}Fn\left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{dom}{\upharpoonright }_{𝑡}=\mathrm{V}\times \mathrm{V}$$
4	2 3	ax-mp	$$⊢\mathrm{dom}{\upharpoonright }_{𝑡}=\mathrm{V}\times \mathrm{V}$$
5	4	ndmov	$$⊢\neg \left(J\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to J{\upharpoonright }_{𝑡}A=\varnothing$$
6	1 5	nsyl2	$$⊢x\in \left(J{\upharpoonright }_{𝑡}A\right)\to \left(J\in \mathrm{V}\wedge A\in \mathrm{V}\right)$$
7		elrest	$$⊢\left(J\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(x\in \left(J{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists y\in Jx=y\cap A\right)$$
8	6 7	syl	$$⊢x\in \left(J{\upharpoonright }_{𝑡}A\right)\to \left(x\in \left(J{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists y\in Jx=y\cap A\right)$$
9	8	ibi	$$⊢x\in \left(J{\upharpoonright }_{𝑡}A\right)\to \exists y\in Jx=y\cap A$$
10		inss2	$$⊢y\cap A\subseteq A$$
11		sseq1	$$⊢x=y\cap A\to \left(x\subseteq A\leftrightarrow y\cap A\subseteq A\right)$$
12	10 11	mpbiri	$$⊢x=y\cap A\to x\subseteq A$$
13	12	rexlimivw	$$⊢\exists y\in Jx=y\cap A\to x\subseteq A$$
14	9 13	syl	$$⊢x\in \left(J{\upharpoonright }_{𝑡}A\right)\to x\subseteq A$$
15		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
16	14 15	sylibr	$$⊢x\in \left(J{\upharpoonright }_{𝑡}A\right)\to x\in 𝒫A$$
17	16	ssriv	$$⊢J{\upharpoonright }_{𝑡}A\subseteq 𝒫A$$