Theorem msubf

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

	Ref	Expression
Hypotheses	msubco.s	$$⊢S=\mathrm{mSubst}\left(T\right)$$
	msubf.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
Assertion	msubf	$$⊢F\in \mathrm{ran}S\to F:E⟶E$$

Proof

Step	Hyp	Ref	Expression
1		msubco.s	$$⊢S=\mathrm{mSubst}\left(T\right)$$
2		msubf.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
3		n0i	$$⊢F\in \mathrm{ran}S\to \neg \mathrm{ran}S=\varnothing$$
4	1	rnfvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{ran}S=\varnothing$$
5	3 4	nsyl2	$$⊢F\in \mathrm{ran}S\to T\in \mathrm{V}$$
6		eqid	$$⊢\mathrm{mVR}\left(T\right)=\mathrm{mVR}\left(T\right)$$
7		eqid	$$⊢\mathrm{mREx}\left(T\right)=\mathrm{mREx}\left(T\right)$$
8	6 7 1 2	msubff	$$⊢T\in \mathrm{V}\to S:\mathrm{mREx}\left(T\right){\uparrow }_{𝑝𝑚}\mathrm{mVR}\left(T\right)⟶E^E$$
9		frn	$$⊢S:\mathrm{mREx}\left(T\right){\uparrow }_{𝑝𝑚}\mathrm{mVR}\left(T\right)⟶E^E\to \mathrm{ran}S\subseteq E^E$$
10	5 8 9	3syl	$$⊢F\in \mathrm{ran}S\to \mathrm{ran}S\subseteq E^E$$
11		id	$$⊢F\in \mathrm{ran}S\to F\in \mathrm{ran}S$$
12	10 11	sseldd	$$⊢F\in \mathrm{ran}S\to F\in \left(E^E\right)$$
13		elmapi	$$⊢F\in \left(E^E\right)\to F:E⟶E$$
14	12 13	syl	$$⊢F\in \mathrm{ran}S\to F:E⟶E$$