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 e. ( 0 ..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )
Assertion fargshiftf 
|- ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> G : ( 0 ..^ ( # ` F ) ) --> dom E )

Proof

Step Hyp Ref Expression
1 fargshift.g 
 |-  G = ( x e. ( 0 ..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )
2 ffn 
 |-  ( F : ( 1 ... N ) --> dom E -> F Fn ( 1 ... N ) )
3 fseq1hash 
 |-  ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( # ` F ) = N )
4 2 3 sylan2 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( # ` F ) = N )
5 eleq1 
 |-  ( N = ( # ` F ) -> ( N e. NN0 <-> ( # ` F ) e. NN0 ) )
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 e. NN0 /\ F : ( 1 ... N ) --> dom E ) <-> ( ( # ` F ) e. NN0 /\ F : ( 1 ... ( # ` F ) ) --> dom E ) ) )
9 8 eqcoms 
 |-  ( ( # ` F ) = N -> ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) <-> ( ( # ` F ) e. NN0 /\ F : ( 1 ... ( # ` F ) ) --> dom E ) ) )
10 fz0add1fz1 
 |-  ( ( ( # ` F ) e. NN0 /\ x e. ( 0 ..^ ( # ` F ) ) ) -> ( x + 1 ) e. ( 1 ... ( # ` F ) ) )
11 ffvelcdm 
 |-  ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( x + 1 ) e. ( 1 ... ( # ` F ) ) ) -> ( F ` ( x + 1 ) ) e. dom E )
12 11 expcom 
 |-  ( ( x + 1 ) e. ( 1 ... ( # ` F ) ) -> ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( F ` ( x + 1 ) ) e. dom E ) )
13 10 12 syl 
 |-  ( ( ( # ` F ) e. NN0 /\ x e. ( 0 ..^ ( # ` F ) ) ) -> ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( F ` ( x + 1 ) ) e. dom E ) )
14 13 impancom 
 |-  ( ( ( # ` F ) e. NN0 /\ F : ( 1 ... ( # ` F ) ) --> dom E ) -> ( x e. ( 0 ..^ ( # ` F ) ) -> ( F ` ( x + 1 ) ) e. dom E ) )
15 14 ralrimiv 
 |-  ( ( ( # ` F ) e. NN0 /\ F : ( 1 ... ( # ` F ) ) --> dom E ) -> A. x e. ( 0 ..^ ( # ` F ) ) ( F ` ( x + 1 ) ) e. dom E )
16 9 15 biimtrdi 
 |-  ( ( # ` F ) = N -> ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> A. x e. ( 0 ..^ ( # ` F ) ) ( F ` ( x + 1 ) ) e. dom E ) )
17 4 16 mpcom 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> A. x e. ( 0 ..^ ( # ` F ) ) ( F ` ( x + 1 ) ) e. dom E )
18 1 fmpt 
 |-  ( A. x e. ( 0 ..^ ( # ` F ) ) ( F ` ( x + 1 ) ) e. dom E <-> G : ( 0 ..^ ( # ` F ) ) --> dom E )
19 17 18 sylib 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> G : ( 0 ..^ ( # ` F ) ) --> dom E )