Metamath Proof Explorer

Theorem mvtinf

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

Ref Expression
Hypotheses mvtinf.f ⊢ F = mVT ⁡ T
mvtinf.y ⊢ Y = mType ⁡ T
Assertion mvtinf ⊢ T ∈ mFS ∧ X ∈ F → ¬ Y -1 X ∈ Fin

Proof

Step Hyp Ref Expression
1 mvtinf.f ⊢ F = mVT ⁡ T
2 mvtinf.y ⊢ Y = mType ⁡ T
3 eqid ⊢ mCN ⁡ T = mCN ⁡ T
4 eqid ⊢ mVR ⁡ T = mVR ⁡ T
5 eqid ⊢ mTC ⁡ T = mTC ⁡ T
6 eqid ⊢ mAx ⁡ T = mAx ⁡ T
7 eqid ⊢ mStat ⁡ T = mStat ⁡ T
8 3 4 2 1 5 6 7 ismfs ⊢ T ∈ mFS → T ∈ mFS ↔ mCN ⁡ T ∩ mVR ⁡ T = ∅ ∧ Y : mVR ⁡ T ⟶ mTC ⁡ T ∧ mAx ⁡ T ⊆ mStat ⁡ T ∧ ∀ v ∈ F ¬ Y -1 v ∈ Fin
9 8 ibi ⊢ T ∈ mFS → mCN ⁡ T ∩ mVR ⁡ T = ∅ ∧ Y : mVR ⁡ T ⟶ mTC ⁡ T ∧ mAx ⁡ T ⊆ mStat ⁡ T ∧ ∀ v ∈ F ¬ Y -1 v ∈ Fin
10 9 simprrd ⊢ T ∈ mFS → ∀ v ∈ F ¬ Y -1 v ∈ Fin
11 sneq ⊢ v = X → v = X
12 11 imaeq2d ⊢ v = X → Y -1 v = Y -1 X
13 12 eleq1d ⊢ v = X → Y -1 v ∈ Fin ↔ Y -1 X ∈ Fin
14 13 notbid ⊢ v = X → ¬ Y -1 v ∈ Fin ↔ ¬ Y -1 X ∈ Fin
15 14 rspccva ⊢ ∀ v ∈ F ¬ Y -1 v ∈ Fin ∧ X ∈ F → ¬ Y -1 X ∈ Fin
16 10 15 sylan ⊢ T ∈ mFS ∧ X ∈ F → ¬ Y -1 X ∈ Fin