Theorem msubff1o

Description: When restricted to complete mappings, the substitution-producing function is bijective to the set of all substitutions. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubff1.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
	msubff1.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
	msubff1.s	$$⊢S=\mathrm{mSubst}\left(T\right)$$
Assertion	msubff1o	$$⊢T\in \mathrm{mFS}\to \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}S$$

Proof

Step	Hyp	Ref	Expression
1		msubff1.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
2		msubff1.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
3		msubff1.s	$$⊢S=\mathrm{mSubst}\left(T\right)$$
4		eqid	$$⊢\mathrm{mEx}\left(T\right)=\mathrm{mEx}\left(T\right)$$
5	1 2 3 4	msubff1	$$⊢T\in \mathrm{mFS}\to \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1}{⟶}{\mathrm{mEx}\left(T\right)}^{\mathrm{mEx}\left(T\right)}$$
6		f1f1orn	$$⊢\left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1}{⟶}{\mathrm{mEx}\left(T\right)}^{\mathrm{mEx}\left(T\right)}\to \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}\left({S\upharpoonright }_{\left(R^V\right)}\right)$$
7	5 6	syl	$$⊢T\in \mathrm{mFS}\to \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}\left({S\upharpoonright }_{\left(R^V\right)}\right)$$
8	1 2 3	msubrn	$$⊢\mathrm{ran}S=S\left[R^V\right]$$
9		df-ima	$$⊢S\left[R^V\right]=\mathrm{ran}\left({S\upharpoonright }_{\left(R^V\right)}\right)$$
10	8 9	eqtri	$$⊢\mathrm{ran}S=\mathrm{ran}\left({S\upharpoonright }_{\left(R^V\right)}\right)$$
11		f1oeq3	$$⊢\mathrm{ran}S=\mathrm{ran}\left({S\upharpoonright }_{\left(R^V\right)}\right)\to \left(\left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}S\leftrightarrow \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}\left({S\upharpoonright }_{\left(R^V\right)}\right)\right)$$
12	10 11	ax-mp	$$⊢\left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}S\leftrightarrow \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}\left({S\upharpoonright }_{\left(R^V\right)}\right)$$
13	7 12	sylibr	$$⊢T\in \mathrm{mFS}\to \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}S$$