Definition df-rest 12553

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.)

Assertion

Ref	Expression
df-rest	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )

Distinct variable group:   x, j, y

Detailed syntax breakdown of Definition df-rest

Step	Hyp	Ref	Expression
1		crest 12551	. 2 class ↾t
2		vj	. . 3 setvar j
3		vx	. . 3 setvar x
4		cvv 2725	. . 3 class _V
5		vy	. . . . 5 setvar y
6	2	cv 1342	. . . . 5 class j
7	5	cv 1342	. . . . . 6 class y
8	3	cv 1342	. . . . . 6 class x
9	7, 8	cin 3114	. . . . 5 class ( y i^i x )
10	5, 6, 9	cmpt 4042	. . . 4 class ( y e. j |-> ( y i^i x ) )
11	10	crn 4604	. . 3 class ran ( y e. j |-> ( y i^i x ) )
12	2, 3, 4, 4, 11	cmpo 5843	. 2 class ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
13	1, 12	wceq 1343	1 wff ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )

This definition is referenced by:  restfn  12555  restval  12557  restsspw  12561  restrcl  12767  ssrest  12782