Metamath Proof Explorer


Theorem fargshiftf

Description: If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 fargshift.g 𝐺 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↦ ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
2 ffn ( 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸𝐹 Fn ( 1 ... 𝑁 ) )
3 fseq1hash ( ( 𝑁 ∈ ℕ0𝐹 Fn ( 1 ... 𝑁 ) ) → ( ♯ ‘ 𝐹 ) = 𝑁 )
4 2 3 sylan2 ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( ♯ ‘ 𝐹 ) = 𝑁 )
5 eleq1 ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝑁 ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) )
6 oveq2 ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 1 ... 𝑁 ) = ( 1 ... ( ♯ ‘ 𝐹 ) ) )
7 6 feq2d ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸𝐹 : ( 1 ... ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ) )
8 5 7 anbi12d ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ↔ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0𝐹 : ( 1 ... ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ) ) )
9 8 eqcoms ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) ↔ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0𝐹 : ( 1 ... ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ) ) )
10 fz0add1fz1 ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑥 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) )
11 ffvelrn ( ( 𝐹 : ( 1 ... ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ∧ ( 𝑥 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∈ dom 𝐸 )
12 11 expcom ( ( 𝑥 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) → ( 𝐹 : ( 1 ... ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 → ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∈ dom 𝐸 ) )
13 10 12 syl ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 : ( 1 ... ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 → ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∈ dom 𝐸 ) )
14 13 impancom ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0𝐹 : ( 1 ... ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∈ dom 𝐸 ) )
15 14 ralrimiv ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0𝐹 : ( 1 ... ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∈ dom 𝐸 )
16 9 15 syl6bi ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∈ dom 𝐸 ) )
17 4 16 mpcom ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∈ dom 𝐸 )
18 1 fmpt ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∈ dom 𝐸𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 )
19 17 18 sylib ( ( 𝑁 ∈ ℕ0𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 )