Metamath Proof Explorer


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 W S R V : R 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 W S R V : R V 1-1 R R
5 f1f1orn S R V : R V 1-1 R R S R V : R V 1-1 onto ran S R V
6 4 5 syl T W S R V : R V 1-1 onto ran S R V
7 1 2 3 mrsubrn ran S = S R V
8 df-ima S R V = ran S R V
9 7 8 eqtri ran S = ran S R V
10 f1oeq3 ran S = ran S R V S R V : R V 1-1 onto ran S S R V : R V 1-1 onto ran S R V
11 9 10 ax-mp S R V : R V 1-1 onto ran S S R V : R V 1-1 onto ran S R V
12 6 11 sylibr T W S R V : R V 1-1 onto ran S