Definition df-rest

Description: Function returning the subspace topology induced by the topology y and the set x . (Contributed by FL, 20-Sep-2010) (Revised by Mario Carneiro, 1-May-2015)

	Ref	Expression
Assertion	df-rest	$$⊢{\upharpoonright }_{𝑡}=\left(j\in \mathrm{V},x\in \mathrm{V}⟼\mathrm{ran}\left(y\in j⟼y\cap x\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crest	$$class{\upharpoonright }_{𝑡}$$
1		vj	$$setvarj$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		vy	$$setvary$$
5	1	cv	$$setvarj$$
6	4	cv	$$setvary$$
7	3	cv	$$setvarx$$
8	6 7	cin	$$class\left(y\cap x\right)$$
9	4 5 8	cmpt	$$class\left(y\in j⟼y\cap x\right)$$
10	9	crn	$$class\mathrm{ran}\left(y\in j⟼y\cap x\right)$$
11	1 3 2 2 10	cmpo	$$class\left(j\in \mathrm{V},x\in \mathrm{V}⟼\mathrm{ran}\left(y\in j⟼y\cap x\right)\right)$$
12	0 11	wceq	$$wff{\upharpoonright }_{𝑡}=\left(j\in \mathrm{V},x\in \mathrm{V}⟼\mathrm{ran}\left(y\in j⟼y\cap x\right)\right)$$