Theorem msubf

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

	Ref	Expression
Hypotheses	msubco.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
	msubf.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
Assertion	msubf	⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 : 𝐸 ⟶ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		msubco.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
2		msubf.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		n0i	⊢ ( 𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅ )
4	1	rnfvprc	⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 = ∅ )
5	3 4	nsyl2	⊢ ( 𝐹 ∈ ran 𝑆 → 𝑇 ∈ V )
6		eqid	⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
7		eqid	⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 )
8	6 7 1 2	msubff	⊢ ( 𝑇 ∈ V → 𝑆 : ( ( mREx ‘ 𝑇 ) ↑pm ( mVR ‘ 𝑇 ) ) ⟶ ( 𝐸 ↑m 𝐸 ) )
9		frn	⊢ ( 𝑆 : ( ( mREx ‘ 𝑇 ) ↑pm ( mVR ‘ 𝑇 ) ) ⟶ ( 𝐸 ↑m 𝐸 ) → ran 𝑆 ⊆ ( 𝐸 ↑m 𝐸 ) )
10	5 8 9	3syl	⊢ ( 𝐹 ∈ ran 𝑆 → ran 𝑆 ⊆ ( 𝐸 ↑m 𝐸 ) )
11		id	⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 ∈ ran 𝑆 )
12	10 11	sseldd	⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 ∈ ( 𝐸 ↑m 𝐸 ) )
13		elmapi	⊢ ( 𝐹 ∈ ( 𝐸 ↑m 𝐸 ) → 𝐹 : 𝐸 ⟶ 𝐸 )
14	12 13	syl	⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 : 𝐸 ⟶ 𝐸 )