Theorem mvtinf

Description: Each variable typecode has infinitely many variables. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mvtinf.f	⊢ 𝐹 = ( mVT ‘ 𝑇 )
	mvtinf.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
Assertion	mvtinf	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑋 ∈ 𝐹 ) → ¬ ( ◡ 𝑌 “ { 𝑋 } ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		mvtinf.f	⊢ 𝐹 = ( mVT ‘ 𝑇 )
2		mvtinf.y	⊢ 𝑌 = ( mType ‘ 𝑇 )
3		eqid	⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
4		eqid	⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
5		eqid	⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 )
6		eqid	⊢ ( mAx ‘ 𝑇 ) = ( mAx ‘ 𝑇 )
7		eqid	⊢ ( mStat ‘ 𝑇 ) = ( mStat ‘ 𝑇 )
8	3 4 2 1 5 6 7	ismfs	⊢ ( 𝑇 ∈ mFS → ( 𝑇 ∈ mFS ↔ ( ( ( ( mCN ‘ 𝑇 ) ∩ ( mVR ‘ 𝑇 ) ) = ∅ ∧ 𝑌 : ( mVR ‘ 𝑇 ) ⟶ ( mTC ‘ 𝑇 ) ) ∧ ( ( mAx ‘ 𝑇 ) ⊆ ( mStat ‘ 𝑇 ) ∧ ∀ 𝑣 ∈ 𝐹 ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) ) ) )
9	8	ibi	⊢ ( 𝑇 ∈ mFS → ( ( ( ( mCN ‘ 𝑇 ) ∩ ( mVR ‘ 𝑇 ) ) = ∅ ∧ 𝑌 : ( mVR ‘ 𝑇 ) ⟶ ( mTC ‘ 𝑇 ) ) ∧ ( ( mAx ‘ 𝑇 ) ⊆ ( mStat ‘ 𝑇 ) ∧ ∀ 𝑣 ∈ 𝐹 ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ) ) )
10	9	simprrd	⊢ ( 𝑇 ∈ mFS → ∀ 𝑣 ∈ 𝐹 ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin )
11		sneq	⊢ ( 𝑣 = 𝑋 → { 𝑣 } = { 𝑋 } )
12	11	imaeq2d	⊢ ( 𝑣 = 𝑋 → ( ◡ 𝑌 “ { 𝑣 } ) = ( ◡ 𝑌 “ { 𝑋 } ) )
13	12	eleq1d	⊢ ( 𝑣 = 𝑋 → ( ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ↔ ( ◡ 𝑌 “ { 𝑋 } ) ∈ Fin ) )
14	13	notbid	⊢ ( 𝑣 = 𝑋 → ( ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ↔ ¬ ( ◡ 𝑌 “ { 𝑋 } ) ∈ Fin ) )
15	14	rspccva	⊢ ( ( ∀ 𝑣 ∈ 𝐹 ¬ ( ◡ 𝑌 “ { 𝑣 } ) ∈ Fin ∧ 𝑋 ∈ 𝐹 ) → ¬ ( ◡ 𝑌 “ { 𝑋 } ) ∈ Fin )
16	10 15	sylan	⊢ ( ( 𝑇 ∈ mFS ∧ 𝑋 ∈ 𝐹 ) → ¬ ( ◡ 𝑌 “ { 𝑋 } ) ∈ Fin )