Theorem mrsubf

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

	Ref	Expression
Hypotheses	mrsubccat.s	$$⊢S=\mathrm{mRSubst}\left(T\right)$$
	mrsubccat.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
Assertion	mrsubf	$$⊢F\in \mathrm{ran}S\to F:R⟶R$$

Proof

Step	Hyp	Ref	Expression
1		mrsubccat.s	$$⊢S=\mathrm{mRSubst}\left(T\right)$$
2		mrsubccat.r	$$⊢R=\mathrm{mREx}\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	6 2 1	mrsubff	$$⊢T\in \mathrm{V}\to S:R{\uparrow }_{𝑝𝑚}\mathrm{mVR}\left(T\right)⟶R^R$$
8		frn	$$⊢S:R{\uparrow }_{𝑝𝑚}\mathrm{mVR}\left(T\right)⟶R^R\to \mathrm{ran}S\subseteq R^R$$
9	5 7 8	3syl	$$⊢F\in \mathrm{ran}S\to \mathrm{ran}S\subseteq R^R$$
10		id	$$⊢F\in \mathrm{ran}S\to F\in \mathrm{ran}S$$
11	9 10	sseldd	$$⊢F\in \mathrm{ran}S\to F\in \left(R^R\right)$$
12		elmapi	$$⊢F\in \left(R^R\right)\to F:R⟶R$$
13	11 12	syl	$$⊢F\in \mathrm{ran}S\to F:R⟶R$$