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