Metamath Proof Explorer


Theorem fargshiftfv

Description: If a class is a function, then the values of the "shifted function" correspond to the function values of the class. (Contributed by Alexander van der Vekens, 23-Nov-2017)

Ref Expression
Hypothesis fargshift.g 𝐺 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↦ ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
Assertion fargshiftfv ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺𝑋 ) = ( 𝐹 ‘ ( 𝑋 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fargshift.g 𝐺 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↦ ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
2 ffn ( 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸𝐹 Fn ( 1 ... 𝑁 ) )
3 fseq1hash ( ( 𝑁 ∈ ℕ0𝐹 Fn ( 1 ... 𝑁 ) ) → ( ♯ ‘ 𝐹 ) = 𝑁 )
4 oveq2 ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5 4 eqcoms ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
6 5 eleq2d ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( 𝑋 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
7 6 biimpd ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
8 3 7 syl ( ( 𝑁 ∈ ℕ0𝐹 Fn ( 1 ... 𝑁 ) ) → ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
9 2 8 sylan2 ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
10 9 imp ( ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑋 ∈ ( 0 ..^ 𝑁 ) ) → 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
11 fvex ( 𝐹 ‘ ( 𝑋 + 1 ) ) ∈ V
12 fvoveq1 ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 𝑥 + 1 ) ) = ( 𝐹 ‘ ( 𝑋 + 1 ) ) )
13 12 1 fvmptg ( ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( 𝐹 ‘ ( 𝑋 + 1 ) ) ∈ V ) → ( 𝐺𝑋 ) = ( 𝐹 ‘ ( 𝑋 + 1 ) ) )
14 10 11 13 sylancl ( ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ∧ 𝑋 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺𝑋 ) = ( 𝐹 ‘ ( 𝑋 + 1 ) ) )
15 14 ex ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺𝑋 ) = ( 𝐹 ‘ ( 𝑋 + 1 ) ) ) )