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 = ( mVR ` T )
	mrsubvr.r	|- R = ( mREx ` T )
	mrsubvr.s	|- S = ( mRSubst ` T )
Assertion	mrsubff1o	|- ( T e. W -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran S )

Proof

Step	Hyp	Ref	Expression
1		mrsubvr.v	|- V = ( mVR ` T )
2		mrsubvr.r	|- R = ( mREx ` T )
3		mrsubvr.s	|- S = ( mRSubst ` T )
4	1 2 3	mrsubff1	|- ( T e. W -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( R ^m R ) )
5		f1f1orn	|- ( ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( R ^m R ) -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran ( S |` ( R ^m V ) ) )
6	4 5	syl	|- ( T e. W -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran ( S |` ( R ^m V ) ) )
7	1 2 3	mrsubrn	|- ran S = ( S " ( R ^m V ) )
8		df-ima	|- ( S " ( R ^m V ) ) = ran ( S |` ( R ^m V ) )
9	7 8	eqtri	|- ran S = ran ( S |` ( R ^m V ) )
10		f1oeq3	|- ( ran S = ran ( S |` ( R ^m V ) ) -> ( ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran S <-> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran ( S |` ( R ^m V ) ) ) )
11	9 10	ax-mp	|- ( ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran S <-> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran ( S |` ( R ^m V ) ) )
12	6 11	sylibr	|- ( T e. W -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran S )