Metamath Proof Explorer

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 \in (0 ..^\|F\|) ⟼ F (x + 1))$
	Assertion	fargshiftfv	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to (X \in (0 ..^N) \to G (X) = F (X + 1))$

Proof

Step	Hyp	Ref	Expression
1		fargshift.g	$⊢ G = (x \in (0 ..^\|F\|) ⟼ F (x + 1))$
2		ffn	$⊢ F : (1 \dots N) ⟶ dom E \to F Fn (1 \dots N)$
3		fseq1hash	$⊢ (N \in ℕ_{0} \land F Fn (1 \dots N)) \to \|F\| = N$
4		oveq2	$⊢ N = \|F\| \to (0 ..^N) = (0 ..^\|F\|)$
5	4	eqcoms	$⊢ \|F\| = N \to (0 ..^N) = (0 ..^\|F\|)$
6	5	eleq2d	$⊢ \|F\| = N \to (X \in (0 ..^N) \leftrightarrow X \in (0 ..^\|F\|))$
7	6	biimpd	$⊢ \|F\| = N \to (X \in (0 ..^N) \to X \in (0 ..^\|F\|))$
8	3 7	syl	$⊢ (N \in ℕ_{0} \land F Fn (1 \dots N)) \to (X \in (0 ..^N) \to X \in (0 ..^\|F\|))$
9	2 8	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to (X \in (0 ..^N) \to X \in (0 ..^\|F\|))$
10	9	imp	$⊢ ((N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \land X \in (0 ..^N)) \to X \in (0 ..^\|F\|)$
11		fvex	$⊢ F (X + 1) \in V$
12		fvoveq1	$⊢ x = X \to F (x + 1) = F (X + 1)$
13	12 1	fvmptg	$⊢ (X \in (0 ..^\|F\|) \land F (X + 1) \in V) \to G (X) = F (X + 1)$
14	10 11 13	sylancl	$⊢ ((N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \land X \in (0 ..^N)) \to G (X) = F (X + 1)$
15	14	ex	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to (X \in (0 ..^N) \to G (X) = F (X + 1))$