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 ffvelcdm ⊢ ( ( 𝐹 : ( 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 biimtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ( 𝑁 ∈ ℕ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 𝐸 )