Theorem mrsubf

Description: A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrsubccat.s	|- S = ( mRSubst ` T )
	mrsubccat.r	|- R = ( mREx ` T )
Assertion	mrsubf	|- ( F e. ran S -> F : R --> R )

Proof

Step	Hyp	Ref	Expression
1		mrsubccat.s	|- S = ( mRSubst ` T )
2		mrsubccat.r	|- R = ( mREx ` T )
3		n0i	|- ( F e. ran S -> -. ran S = (/) )
4	1	rnfvprc	|- ( -. T e. _V -> ran S = (/) )
5	3 4	nsyl2	|- ( F e. ran S -> T e. _V )
6		eqid	|- ( mVR ` T ) = ( mVR ` T )
7	6 2 1	mrsubff	|- ( T e. _V -> S : ( R ^pm ( mVR ` T ) ) --> ( R ^m R ) )
8		frn	|- ( S : ( R ^pm ( mVR ` T ) ) --> ( R ^m R ) -> ran S C_ ( R ^m R ) )
9	5 7 8	3syl	|- ( F e. ran S -> ran S C_ ( R ^m R ) )
10		id	|- ( F e. ran S -> F e. ran S )
11	9 10	sseldd	|- ( F e. ran S -> F e. ( R ^m R ) )
12		elmapi	|- ( F e. ( R ^m R ) -> F : R --> R )
13	11 12	syl	|- ( F e. ran S -> F : R --> R )