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 = ( mVR ` T )
	msubff1.r	|- R = ( mREx ` T )
	msubff1.s	|- S = ( mSubst ` T )
Assertion	msubff1o	|- ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran S )

Proof

Step	Hyp	Ref	Expression
1		msubff1.v	|- V = ( mVR ` T )
2		msubff1.r	|- R = ( mREx ` T )
3		msubff1.s	|- S = ( mSubst ` T )
4		eqid	|- ( mEx ` T ) = ( mEx ` T )
5	1 2 3 4	msubff1	|- ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( ( mEx ` T ) ^m ( mEx ` T ) ) )
6		f1f1orn	|- ( ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( ( mEx ` T ) ^m ( mEx ` T ) ) -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran ( S |` ( R ^m V ) ) )
7	5 6	syl	|- ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran ( S |` ( R ^m V ) ) )
8	1 2 3	msubrn	|- ran S = ( S " ( R ^m V ) )
9		df-ima	|- ( S " ( R ^m V ) ) = ran ( S |` ( R ^m V ) )
10	8 9	eqtri	|- ran S = ran ( S |` ( R ^m V ) )
11		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 ) ) ) )
12	10 11	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 ) ) )
13	7 12	sylibr	|- ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-onto-> ran S )