Theorem msubf

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

	Ref	Expression
Hypotheses	msubco.s	|- S = ( mSubst ` T )
	msubf.e	|- E = ( mEx ` T )
Assertion	msubf	|- ( F e. ran S -> F : E --> E )

Proof

Step	Hyp	Ref	Expression
1		msubco.s	|- S = ( mSubst ` T )
2		msubf.e	|- E = ( mEx ` 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		eqid	|- ( mREx ` T ) = ( mREx ` T )
8	6 7 1 2	msubff	|- ( T e. _V -> S : ( ( mREx ` T ) ^pm ( mVR ` T ) ) --> ( E ^m E ) )
9		frn	|- ( S : ( ( mREx ` T ) ^pm ( mVR ` T ) ) --> ( E ^m E ) -> ran S C_ ( E ^m E ) )
10	5 8 9	3syl	|- ( F e. ran S -> ran S C_ ( E ^m E ) )
11		id	|- ( F e. ran S -> F e. ran S )
12	10 11	sseldd	|- ( F e. ran S -> F e. ( E ^m E ) )
13		elmapi	|- ( F e. ( E ^m E ) -> F : E --> E )
14	12 13	syl	|- ( F e. ran S -> F : E --> E )