Theorem mrsubff1o

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	mrsubvr.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
	mrsubvr.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
	mrsubvr.s	$$⊢S=\mathrm{mRSubst}\left(T\right)$$
Assertion	mrsubff1o	$$⊢T\in W\to \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}S$$

Proof

Step	Hyp	Ref	Expression
1		mrsubvr.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
2		mrsubvr.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
3		mrsubvr.s	$$⊢S=\mathrm{mRSubst}\left(T\right)$$
4	1 2 3	mrsubff1	$$⊢T\in W\to \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1}{⟶}{R}^R$$
5		f1f1orn	$$⊢\left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1}{⟶}{R}^R\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)$$
6	4 5	syl	$$⊢T\in W\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	1 2 3	mrsubrn	$$⊢\mathrm{ran}S=S\left[R^V\right]$$
8		df-ima	$$⊢S\left[R^V\right]=\mathrm{ran}\left({S\upharpoonright }_{\left(R^V\right)}\right)$$
9	7 8	eqtri	$$⊢\mathrm{ran}S=\mathrm{ran}\left({S\upharpoonright }_{\left(R^V\right)}\right)$$
10		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)$$
11	9 10	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)$$
12	6 11	sylibr	$$⊢T\in W\to \left({S\upharpoonright }_{\left(R^V\right)}\right):R^V\underset{1-1\; onto}{⟶}\mathrm{ran}S$$