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	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mrsubvr.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	mrsubvr.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
Assertion	mrsubff1o	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1-onto→ ran 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		mrsubvr.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mrsubvr.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
3		mrsubvr.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
4	1 2 3	mrsubff1	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝑅 ↑m 𝑅 ) )
5		f1f1orn	⊢ ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝑅 ↑m 𝑅 ) → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1-onto→ ran ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) )
6	4 5	syl	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1-onto→ ran ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) )
7	1 2 3	mrsubrn	⊢ ran 𝑆 = ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) )
8		df-ima	⊢ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) = ran ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) )
9	7 8	eqtri	⊢ ran 𝑆 = ran ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) )
10		f1oeq3	⊢ ( ran 𝑆 = ran ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1-onto→ ran 𝑆 ↔ ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1-onto→ ran ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ) )
11	9 10	ax-mp	⊢ ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1-onto→ ran 𝑆 ↔ ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1-onto→ ran ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) )
12	6 11	sylibr	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1-onto→ ran 𝑆 )