Theorem mtyf

Description: The type function maps variables to variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mtyf.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mtyf.f	⊢ 𝐹 = ( mVT ‘ 𝑇 )
	mtyf.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
Assertion	mtyf	⊢ ( 𝑇 ∈ mFS → 𝑌 : 𝑉 ⟶ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		mtyf.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mtyf.f	⊢ 𝐹 = ( mVT ‘ 𝑇 )
3		mtyf.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
4		eqid	⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 )
5	1 4 3	mtyf2	⊢ ( 𝑇 ∈ mFS → 𝑌 : 𝑉 ⟶ ( mTC ‘ 𝑇 ) )
6		ffn	⊢ ( 𝑌 : 𝑉 ⟶ ( mTC ‘ 𝑇 ) → 𝑌 Fn 𝑉 )
7		dffn4	⊢ ( 𝑌 Fn 𝑉 ↔ 𝑌 : 𝑉 –onto→ ran 𝑌 )
8	6 7	sylib	⊢ ( 𝑌 : 𝑉 ⟶ ( mTC ‘ 𝑇 ) → 𝑌 : 𝑉 –onto→ ran 𝑌 )
9		fof	⊢ ( 𝑌 : 𝑉 –onto→ ran 𝑌 → 𝑌 : 𝑉 ⟶ ran 𝑌 )
10	5 8 9	3syl	⊢ ( 𝑇 ∈ mFS → 𝑌 : 𝑉 ⟶ ran 𝑌 )
11	2 3	mvtval	⊢ 𝐹 = ran 𝑌
12		feq3	⊢ ( 𝐹 = ran 𝑌 → ( 𝑌 : 𝑉 ⟶ 𝐹 ↔ 𝑌 : 𝑉 ⟶ ran 𝑌 ) )
13	11 12	ax-mp	⊢ ( 𝑌 : 𝑉 ⟶ 𝐹 ↔ 𝑌 : 𝑉 ⟶ ran 𝑌 )
14	10 13	sylibr	⊢ ( 𝑇 ∈ mFS → 𝑌 : 𝑉 ⟶ 𝐹 )