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

Proof

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