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 ⊢ 𝑉 = ( mVR ‘ 𝑇 )
mvrsval.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
mvrsval.w ⊢ 𝑊 = ( mVars ‘ 𝑇 )
Assertion mvrsfpw ( 𝑋 ∈ 𝐸 → ( 𝑊 ‘ 𝑋 ) ∈ ( 𝒫 𝑉 ∩ Fin ) )

Proof

Step Hyp Ref Expression
1 mvrsval.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
2 mvrsval.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
3 mvrsval.w ⊢ 𝑊 = ( mVars ‘ 𝑇 )
4 1 2 3 mvrsval ⊢ ( 𝑋 ∈ 𝐸 → ( 𝑊 ‘ 𝑋 ) = ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) )
5 inss2 ⊢ ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ⊆ 𝑉
6 5 a1i ⊢ ( 𝑋 ∈ 𝐸 → ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ⊆ 𝑉 )
7 fzofi ⊢ ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) ∈ Fin
8 xp2nd ⊢ ( 𝑋 ∈ ( ( mTC ‘ 𝑇 ) × Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) → ( 2nd ‘ 𝑋 ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
9 eqid ⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 )
10 eqid ⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
11 9 2 10 1 mexval2 ⊢ 𝐸 = ( ( mTC ‘ 𝑇 ) × Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
12 8 11 eleq2s ⊢ ( 𝑋 ∈ 𝐸 → ( 2nd ‘ 𝑋 ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
13 wrdf ⊢ ( ( 2nd ‘ 𝑋 ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) → ( 2nd ‘ 𝑋 ) : ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) ⟶ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
14 ffn ⊢ ( ( 2nd ‘ 𝑋 ) : ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) ⟶ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) → ( 2nd ‘ 𝑋 ) Fn ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) )
15 12 13 14 3syl ⊢ ( 𝑋 ∈ 𝐸 → ( 2nd ‘ 𝑋 ) Fn ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) )
16 dffn4 ⊢ ( ( 2nd ‘ 𝑋 ) Fn ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) ↔ ( 2nd ‘ 𝑋 ) : ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) –onto→ ran ( 2nd ‘ 𝑋 ) )
17 15 16 sylib ⊢ ( 𝑋 ∈ 𝐸 → ( 2nd ‘ 𝑋 ) : ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) –onto→ ran ( 2nd ‘ 𝑋 ) )
18 fofi ⊢ ( ( ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) ∈ Fin ∧ ( 2nd ‘ 𝑋 ) : ( 0 ..^ ( ♯ ‘ ( 2nd ‘ 𝑋 ) ) ) –onto→ ran ( 2nd ‘ 𝑋 ) ) → ran ( 2nd ‘ 𝑋 ) ∈ Fin )
19 7 17 18 sylancr ⊢ ( 𝑋 ∈ 𝐸 → ran ( 2nd ‘ 𝑋 ) ∈ Fin )
20 inss1 ⊢ ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ⊆ ran ( 2nd ‘ 𝑋 )
21 ssfi ⊢ ( ( ran ( 2nd ‘ 𝑋 ) ∈ Fin ∧ ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ⊆ ran ( 2nd ‘ 𝑋 ) ) → ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ∈ Fin )
22 19 20 21 sylancl ⊢ ( 𝑋 ∈ 𝐸 → ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ∈ Fin )
23 elfpw ⊢ ( ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ∈ ( 𝒫 𝑉 ∩ Fin ) ↔ ( ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ⊆ 𝑉 ∧ ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ∈ Fin ) )
24 6 22 23 sylanbrc ⊢ ( 𝑋 ∈ 𝐸 → ( ran ( 2nd ‘ 𝑋 ) ∩ 𝑉 ) ∈ ( 𝒫 𝑉 ∩ Fin ) )
25 4 24 eqeltrd ⊢ ( 𝑋 ∈ 𝐸 → ( 𝑊 ‘ 𝑋 ) ∈ ( 𝒫 𝑉 ∩ Fin ) )