Metamath Proof Explorer

Theorem mvrsfpw

Description: The set of variables in an expression is a finite subset of V . (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mvrsval.v 
|- V = ( mVR ` T )
mvrsval.e 
|- E = ( mEx ` T )
mvrsval.w 
|- W = ( mVars ` T )
Assertion mvrsfpw 
|- ( X e. E -> ( W ` X ) e. ( ~P V i^i Fin ) )

Proof

Step Hyp Ref Expression
1 mvrsval.v 
 |-  V = ( mVR ` T )
2 mvrsval.e 
 |-  E = ( mEx ` T )
3 mvrsval.w 
 |-  W = ( mVars ` T )
4 1 2 3 mvrsval 
 |-  ( X e. E -> ( W ` X ) = ( ran ( 2nd ` X ) i^i V ) )
5 inss2 
 |-  ( ran ( 2nd ` X ) i^i V ) C_ V
6 5 a1i 
 |-  ( X e. E -> ( ran ( 2nd ` X ) i^i V ) C_ V )
7 fzofi 
 |-  ( 0 ..^ ( # ` ( 2nd ` X ) ) ) e. Fin
8 xp2nd 
 |-  ( X e. ( ( mTC ` T ) X. Word ( ( mCN ` T ) u. V ) ) -> ( 2nd ` X ) e. Word ( ( mCN ` T ) u. V ) )
9 eqid 
 |-  ( mTC ` T ) = ( mTC ` T )
10 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
11 9 2 10 1 mexval2 
 |-  E = ( ( mTC ` T ) X. Word ( ( mCN ` T ) u. V ) )
12 8 11 eleq2s 
 |-  ( X e. E -> ( 2nd ` X ) e. Word ( ( mCN ` T ) u. V ) )
13 wrdf 
 |-  ( ( 2nd ` X ) e. Word ( ( mCN ` T ) u. V ) -> ( 2nd ` X ) : ( 0 ..^ ( # ` ( 2nd ` X ) ) ) --> ( ( mCN ` T ) u. V ) )
14 ffn 
 |-  ( ( 2nd ` X ) : ( 0 ..^ ( # ` ( 2nd ` X ) ) ) --> ( ( mCN ` T ) u. V ) -> ( 2nd ` X ) Fn ( 0 ..^ ( # ` ( 2nd ` X ) ) ) )
15 12 13 14 3syl 
 |-  ( X e. E -> ( 2nd ` X ) Fn ( 0 ..^ ( # ` ( 2nd ` X ) ) ) )
16 dffn4 
 |-  ( ( 2nd ` X ) Fn ( 0 ..^ ( # ` ( 2nd ` X ) ) ) <-> ( 2nd ` X ) : ( 0 ..^ ( # ` ( 2nd ` X ) ) ) -onto-> ran ( 2nd ` X ) )
17 15 16 sylib 
 |-  ( X e. E -> ( 2nd ` X ) : ( 0 ..^ ( # ` ( 2nd ` X ) ) ) -onto-> ran ( 2nd ` X ) )
18 fofi 
 |-  ( ( ( 0 ..^ ( # ` ( 2nd ` X ) ) ) e. Fin /\ ( 2nd ` X ) : ( 0 ..^ ( # ` ( 2nd ` X ) ) ) -onto-> ran ( 2nd ` X ) ) -> ran ( 2nd ` X ) e. Fin )
19 7 17 18 sylancr 
 |-  ( X e. E -> ran ( 2nd ` X ) e. Fin )
20 inss1 
 |-  ( ran ( 2nd ` X ) i^i V ) C_ ran ( 2nd ` X )
21 ssfi 
 |-  ( ( ran ( 2nd ` X ) e. Fin /\ ( ran ( 2nd ` X ) i^i V ) C_ ran ( 2nd ` X ) ) -> ( ran ( 2nd ` X ) i^i V ) e. Fin )
22 19 20 21 sylancl 
 |-  ( X e. E -> ( ran ( 2nd ` X ) i^i V ) e. Fin )
23 elfpw 
 |-  ( ( ran ( 2nd ` X ) i^i V ) e. ( ~P V i^i Fin ) <-> ( ( ran ( 2nd ` X ) i^i V ) C_ V /\ ( ran ( 2nd ` X ) i^i V ) e. Fin ) )
24 6 22 23 sylanbrc 
 |-  ( X e. E -> ( ran ( 2nd ` X ) i^i V ) e. ( ~P V i^i Fin ) )
25 4 24 eqeltrd 
 |-  ( X e. E -> ( W ` X ) e. ( ~P V i^i Fin ) )