Theorem mtyf2

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

	Ref	Expression
Hypotheses	mtyf2.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mvtf2.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
	mtyf2.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
Assertion	mtyf2	⊢ ( 𝑇 ∈ mFS → 𝑌 : 𝑉 ⟶ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		mtyf2.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mvtf2.k	⊢ 𝐾 = ( mTC ‘ 𝑇 )
3		mtyf2.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
4		eqid	⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
5		eqid	⊢ ( mVT ‘ 𝑇 ) = ( mVT ‘ 𝑇 )
6		eqid	⊢ ( mAx ‘ 𝑇 ) = ( mAx ‘ 𝑇 )
7		eqid	⊢ ( mStat ‘ 𝑇 ) = ( mStat ‘ 𝑇 )
8	4 1 3 5 2 6 7	ismfs	⊢ ( 𝑇 ∈ mFS → ( 𝑇 ∈ mFS ↔ ( ( ( ( mCN ‘ 𝑇 ) ∩ 𝑉 ) = ∅ ∧ 𝑌 : 𝑉 ⟶ 𝐾 ) ∧ ( ( mAx ‘ 𝑇 ) ⊆ ( mStat ‘ 𝑇 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑇 ) ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) ) ) )
9	8	ibi	⊢ ( 𝑇 ∈ mFS → ( ( ( ( mCN ‘ 𝑇 ) ∩ 𝑉 ) = ∅ ∧ 𝑌 : 𝑉 ⟶ 𝐾 ) ∧ ( ( mAx ‘ 𝑇 ) ⊆ ( mStat ‘ 𝑇 ) ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑇 ) ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) ) )
10	9	simplrd	⊢ ( 𝑇 ∈ mFS → 𝑌 : 𝑉 ⟶ 𝐾 )