Theorem restfn

Description: The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015)

	Ref	Expression
Assertion	restfn	|- |`t Fn ( _V X. _V )

Proof

Step	Hyp	Ref	Expression
1		df-rest	|- |`t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
2		vex	|- j e. _V
3	2	mptex	|- ( y e. j |-> ( y i^i x ) ) e. _V
4	3	rnex	|- ran ( y e. j |-> ( y i^i x ) ) e. _V
5	1 4	fnmpoi	|- |`t Fn ( _V X. _V )