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→W⁡X∈𝒫V∩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→W⁡X=ran⁡2nd⁡X∩V
5 inss2 ⊢ran⁡2nd⁡X∩V⊆V
6 5 a1i ⊢X∈E→ran⁡2nd⁡X∩V⊆V
7 fzofi ⊢0..^2nd⁡X∈Fin
8 xp2nd ⊢X∈mTC⁡T×WordmCN⁡T∪V→2nd⁡X∈WordmCN⁡T∪V
9 eqid ⊢mTC⁡T=mTC⁡T
10 eqid ⊢mCN⁡T=mCN⁡T
11 9 2 10 1 mexval2 ⊢E=mTC⁡T×WordmCN⁡T∪V
12 8 11 eleq2s ⊢X∈E→2nd⁡X∈WordmCN⁡T∪V
13 wrdf ⊢2nd⁡X∈WordmCN⁡T∪V→2nd⁡X:0..^2nd⁡X⟶mCN⁡T∪V
14 ffn ⊢2nd⁡X:0..^2nd⁡X⟶mCN⁡T∪V→2nd⁡XFn0..^2nd⁡X
15 12 13 14 3syl ⊢X∈E→2nd⁡XFn0..^2nd⁡X
16 dffn4 ⊢2nd⁡XFn0..^2nd⁡X↔2nd⁡X:0..^2nd⁡X⟶ontoran⁡2nd⁡X
17 15 16 sylib ⊢X∈E→2nd⁡X:0..^2nd⁡X⟶ontoran⁡2nd⁡X
18 fofi ⊢0..^2nd⁡X∈Fin∧2nd⁡X:0..^2nd⁡X⟶ontoran⁡2nd⁡X→ran⁡2nd⁡X∈Fin
19 7 17 18 sylancr ⊢X∈E→ran⁡2nd⁡X∈Fin
20 inss1 ⊢ran⁡2nd⁡X∩V⊆ran⁡2nd⁡X
21 ssfi ⊢ran⁡2nd⁡X∈Fin∧ran⁡2nd⁡X∩V⊆ran⁡2nd⁡X→ran⁡2nd⁡X∩V∈Fin
22 19 20 21 sylancl ⊢X∈E→ran⁡2nd⁡X∩V∈Fin
23 elfpw ⊢ran⁡2nd⁡X∩V∈𝒫V∩Fin↔ran⁡2nd⁡X∩V⊆V∧ran⁡2nd⁡X∩V∈Fin
24 6 22 23 sylanbrc ⊢X∈E→ran⁡2nd⁡X∩V∈𝒫V∩Fin
25 4 24 eqeltrd ⊢X∈E→W⁡X∈𝒫V∩Fin