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 G = x 0 ..^ F F x + 1
Assertion fargshiftf N 0 F : 1 N dom E G : 0 ..^ F dom E

Proof

Step Hyp Ref Expression
1 fargshift.g G = x 0 ..^ F F x + 1
2 ffn F : 1 N dom E F Fn 1 N
3 fseq1hash N 0 F Fn 1 N F = N
4 2 3 sylan2 N 0 F : 1 N dom E F = N
5 eleq1 N = F N 0 F 0
6 oveq2 N = F 1 N = 1 F
7 6 feq2d N = F F : 1 N dom E F : 1 F dom E
8 5 7 anbi12d N = F N 0 F : 1 N dom E F 0 F : 1 F dom E
9 8 eqcoms F = N N 0 F : 1 N dom E F 0 F : 1 F dom E
10 fz0add1fz1 F 0 x 0 ..^ F x + 1 1 F
11 ffvelrn F : 1 F dom E x + 1 1 F F x + 1 dom E
12 11 expcom x + 1 1 F F : 1 F dom E F x + 1 dom E
13 10 12 syl F 0 x 0 ..^ F F : 1 F dom E F x + 1 dom E
14 13 impancom F 0 F : 1 F dom E x 0 ..^ F F x + 1 dom E
15 14 ralrimiv F 0 F : 1 F dom E x 0 ..^ F F x + 1 dom E
16 9 15 syl6bi F = N N 0 F : 1 N dom E x 0 ..^ F F x + 1 dom E
17 4 16 mpcom N 0 F : 1 N dom E x 0 ..^ F F x + 1 dom E
18 1 fmpt x 0 ..^ F F x + 1 dom E G : 0 ..^ F dom E
19 17 18 sylib N 0 F : 1 N dom E G : 0 ..^ F dom E