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 e. mFS /\ X e. F ) -> -. ( `' Y " { X } ) e. 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 e. mFS -> ( T e. mFS <-> ( ( ( ( mCN ` T ) i^i ( mVR ` T ) ) = (/) /\ Y : ( mVR ` T ) --> ( mTC ` T ) ) /\ ( ( mAx ` T ) C_ ( mStat ` T ) /\ A. v e. F -. ( `' Y " { v } ) e. Fin ) ) ) )
9 8 ibi 
 |-  ( T e. mFS -> ( ( ( ( mCN ` T ) i^i ( mVR ` T ) ) = (/) /\ Y : ( mVR ` T ) --> ( mTC ` T ) ) /\ ( ( mAx ` T ) C_ ( mStat ` T ) /\ A. v e. F -. ( `' Y " { v } ) e. Fin ) ) )
10 9 simprrd 
 |-  ( T e. mFS -> A. v e. F -. ( `' Y " { v } ) e. Fin )
11 sneq 
 |-  ( v = X -> { v } = { X } )
12 11 imaeq2d 
 |-  ( v = X -> ( `' Y " { v } ) = ( `' Y " { X } ) )
13 12 eleq1d 
 |-  ( v = X -> ( ( `' Y " { v } ) e. Fin <-> ( `' Y " { X } ) e. Fin ) )
14 13 notbid 
 |-  ( v = X -> ( -. ( `' Y " { v } ) e. Fin <-> -. ( `' Y " { X } ) e. Fin ) )
15 14 rspccva 
 |-  ( ( A. v e. F -. ( `' Y " { v } ) e. Fin /\ X e. F ) -> -. ( `' Y " { X } ) e. Fin )
16 10 15 sylan 
 |-  ( ( T e. mFS /\ X e. F ) -> -. ( `' Y " { X } ) e. Fin )