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

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	2 3	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to \|F\| = N$
5		eleq1	$⊢ N = \|F\| \to (N \in ℕ_{0} \leftrightarrow \|F\| \in ℕ_{0})$
6		oveq2	$⊢ N = \|F\| \to (1 \dots N) = (1 \dots \|F\|)$
7	6	feq2d	$⊢ N = \|F\| \to (F : (1 \dots N) ⟶ dom E \leftrightarrow F : (1 \dots \|F\|) ⟶ dom E)$
8	5 7	anbi12d	$⊢ N = \|F\| \to ((N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \leftrightarrow (\|F\| \in ℕ_{0} \land F : (1 \dots \|F\|) ⟶ dom E))$
9	8	eqcoms	$⊢ \|F\| = N \to ((N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \leftrightarrow (\|F\| \in ℕ_{0} \land F : (1 \dots \|F\|) ⟶ dom E))$
10		fz0add1fz1	$⊢ (\|F\| \in ℕ_{0} \land x \in (0 ..^\|F\|)) \to x + 1 \in (1 \dots \|F\|)$
11		ffvelcdm	$⊢ (F : (1 \dots \|F\|) ⟶ dom E \land x + 1 \in (1 \dots \|F\|)) \to F (x + 1) \in dom E$
12	11	expcom	$⊢ x + 1 \in (1 \dots \|F\|) \to (F : (1 \dots \|F\|) ⟶ dom E \to F (x + 1) \in dom E)$
13	10 12	syl	$⊢ (\|F\| \in ℕ_{0} \land x \in (0 ..^\|F\|)) \to (F : (1 \dots \|F\|) ⟶ dom E \to F (x + 1) \in dom E)$
14	13	impancom	$⊢ (\|F\| \in ℕ_{0} \land F : (1 \dots \|F\|) ⟶ dom E) \to (x \in (0 ..^\|F\|) \to F (x + 1) \in dom E)$
15	14	ralrimiv	$⊢ (\|F\| \in ℕ_{0} \land F : (1 \dots \|F\|) ⟶ dom E) \to \forall x \in (0 ..^\|F\|) F (x + 1) \in dom E$
16	9 15	syl6bi	$⊢ \|F\| = N \to ((N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to \forall x \in (0 ..^\|F\|) F (x + 1) \in dom E)$
17	4 16	mpcom	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to \forall x \in (0 ..^\|F\|) F (x + 1) \in dom E$
18	1	fmpt	$⊢ \forall x \in (0 ..^\|F\|) F (x + 1) \in dom E \leftrightarrow G : (0 ..^\|F\|) ⟶ dom E$
19	17 18	sylib	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to G : (0 ..^\|F\|) ⟶ dom E$