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	|- |`t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crest	|- |`t
1		vj	|- j
2		cvv	|- _V
3		vx	|- x
4		vy	|- y
5	1	cv	|- j
6	4	cv	|- y
7	3	cv	|- x
8	6 7	cin	|- ( y i^i x )
9	4 5 8	cmpt	|- ( y e. j |-> ( y i^i x ) )
10	9	crn	|- ran ( y e. j |-> ( y i^i x ) )
11	1 3 2 2 10	cmpo	|- ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
12	0 11	wceq	|- |`t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )