Theorem mrsubf

Description: A substitution is a function. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrsubccat.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
	mrsubccat.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
Assertion	mrsubf	⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 : 𝑅 ⟶ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		mrsubccat.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
2		mrsubccat.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
3		n0i	⊢ ( 𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅ )
4	1	rnfvprc	⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 = ∅ )
5	3 4	nsyl2	⊢ ( 𝐹 ∈ ran 𝑆 → 𝑇 ∈ V )
6		eqid	⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
7	6 2 1	mrsubff	⊢ ( 𝑇 ∈ V → 𝑆 : ( 𝑅 ↑pm ( mVR ‘ 𝑇 ) ) ⟶ ( 𝑅 ↑m 𝑅 ) )
8		frn	⊢ ( 𝑆 : ( 𝑅 ↑pm ( mVR ‘ 𝑇 ) ) ⟶ ( 𝑅 ↑m 𝑅 ) → ran 𝑆 ⊆ ( 𝑅 ↑m 𝑅 ) )
9	5 7 8	3syl	⊢ ( 𝐹 ∈ ran 𝑆 → ran 𝑆 ⊆ ( 𝑅 ↑m 𝑅 ) )
10		id	⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 ∈ ran 𝑆 )
11	9 10	sseldd	⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 ∈ ( 𝑅 ↑m 𝑅 ) )
12		elmapi	⊢ ( 𝐹 ∈ ( 𝑅 ↑m 𝑅 ) → 𝐹 : 𝑅 ⟶ 𝑅 )
13	11 12	syl	⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 : 𝑅 ⟶ 𝑅 )