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

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		oveq2	|- ( N = ( # ` F ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) ) )
5	4	eqcoms	|- ( ( # ` F ) = N -> ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) ) )
6	5	eleq2d	|- ( ( # ` F ) = N -> ( X e. ( 0 ..^ N ) <-> X e. ( 0 ..^ ( # ` F ) ) ) )
7	6	biimpd	|- ( ( # ` F ) = N -> ( X e. ( 0 ..^ N ) -> X e. ( 0 ..^ ( # ` F ) ) ) )
8	3 7	syl	|- ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( X e. ( 0 ..^ N ) -> X e. ( 0 ..^ ( # ` F ) ) ) )
9	2 8	sylan2	|- ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( X e. ( 0 ..^ N ) -> X e. ( 0 ..^ ( # ` F ) ) ) )
10	9	imp	|- ( ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) /\ X e. ( 0 ..^ N ) ) -> X e. ( 0 ..^ ( # ` F ) ) )
11		fvex	|- ( F ` ( X + 1 ) ) e. _V
12		fvoveq1	|- ( x = X -> ( F ` ( x + 1 ) ) = ( F ` ( X + 1 ) ) )
13	12 1	fvmptg	|- ( ( X e. ( 0 ..^ ( # ` F ) ) /\ ( F ` ( X + 1 ) ) e. _V ) -> ( G ` X ) = ( F ` ( X + 1 ) ) )
14	10 11 13	sylancl	|- ( ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) /\ X e. ( 0 ..^ N ) ) -> ( G ` X ) = ( F ` ( X + 1 ) ) )
15	14	ex	|- ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( X e. ( 0 ..^ N ) -> ( G ` X ) = ( F ` ( X + 1 ) ) ) )