fargshiftfo

Description: If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017)

		Ref	Expression
	Hypothesis	fargshift.g	$⊢ G = (x \in (0 ..^\|F\|) ⟼ F (x + 1))$
	Assertion	fargshiftfo	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to G : (0 ..^\|F\|) \underset{onto}{⟶} dom E$

Proof

Step	Hyp	Ref	Expression
1		fargshift.g	$⊢ G = (x \in (0 ..^\|F\|) ⟼ F (x + 1))$
2		fof	$⊢ F : (1 \dots N) \underset{onto}{⟶} dom E \to F : (1 \dots N) ⟶ dom E$
3	1	fargshiftf	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to G : (0 ..^\|F\|) ⟶ dom E$
4	2 3	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to G : (0 ..^\|F\|) ⟶ dom E$
5	1	rnmpt	$⊢ ran G = \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\}$
6		fofn	$⊢ F : (1 \dots N) \underset{onto}{⟶} dom E \to F Fn (1 \dots N)$
7		fnrnfv	$⊢ F Fn (1 \dots N) \to ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\}$
8	6 7	syl	$⊢ F : (1 \dots N) \underset{onto}{⟶} dom E \to ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\}$
9	8	adantl	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\}$
10		df-fo	$⊢ F : (1 \dots N) \underset{onto}{⟶} dom E \leftrightarrow (F Fn (1 \dots N) \land ran F = dom E)$
11	10	bilani	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (F Fn (1 \dots N) \land ran F = dom E)$
12		eqeq1	$⊢ ran F = dom E \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \leftrightarrow dom E = \{y \| \exists z \in (1 \dots N) y = F (z)\})$
13		eqcom	$⊢ dom E = \{y \| \exists z \in (1 \dots N) y = F (z)\} \leftrightarrow \{y \| \exists z \in (1 \dots N) y = F (z)\} = dom E$
14	12 13	bitrdi	$⊢ ran F = dom E \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \leftrightarrow \{y \| \exists z \in (1 \dots N) y = F (z)\} = dom E)$
15		ffn	$⊢ F : (1 \dots N) ⟶ dom E \to F Fn (1 \dots N)$
16		fseq1hash	$⊢ (N \in ℕ_{0} \land F Fn (1 \dots N)) \to \|F\| = N$
17	15 16	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to \|F\| = N$
18	2 17	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \|F\| = N$
19		fz0add1fz1	$⊢ (N \in ℕ_{0} \land x \in (0 ..^N)) \to x + 1 \in (1 \dots N)$
20		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
21		fzval3	$⊢ N \in ℤ \to (1 \dots N) = (1 ..^N + 1)$
22	20 21	syl	$⊢ N \in ℕ_{0} \to (1 \dots N) = (1 ..^N + 1)$
23		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
24		1cnd	$⊢ N \in ℕ_{0} \to 1 \in ℂ$
25	23 24	addcomd	$⊢ N \in ℕ_{0} \to N + 1 = 1 + N$
26	25	oveq2d	$⊢ N \in ℕ_{0} \to (1 ..^N + 1) = (1 ..^1 + N)$
27	22 26	eqtrd	$⊢ N \in ℕ_{0} \to (1 \dots N) = (1 ..^1 + N)$
28	27	eleq2d	$⊢ N \in ℕ_{0} \to (z \in (1 \dots N) \leftrightarrow z \in (1 ..^1 + N))$
29	28	biimpa	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z \in (1 ..^1 + N)$
30	20	adantr	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to N \in ℤ$
31		fzosubel3	$⊢ (z \in (1 ..^1 + N) \land N \in ℤ) \to z - 1 \in (0 ..^N)$
32	29 30 31	syl2anc	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z - 1 \in (0 ..^N)$
33		oveq1	$⊢ x = z - 1 \to x + 1 = z - 1 + 1$
34	33	eqeq2d	$⊢ x = z - 1 \to (z = x + 1 \leftrightarrow z = z - 1 + 1)$
35	34	adantl	$⊢ ((N \in ℕ_{0} \land z \in (1 \dots N)) \land x = z - 1) \to (z = x + 1 \leftrightarrow z = z - 1 + 1)$
36		elfzelz	$⊢ z \in (1 \dots N) \to z \in ℤ$
37	36	zcnd	$⊢ z \in (1 \dots N) \to z \in ℂ$
38	37	adantl	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z \in ℂ$
39		1cnd	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to 1 \in ℂ$
40	38 39	npcand	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z - 1 + 1 = z$
41	40	eqcomd	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z = z - 1 + 1$
42	32 35 41	rspcedvd	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to \exists x \in (0 ..^N) z = x + 1$
43		fveq2	$⊢ z = x + 1 \to F (z) = F (x + 1)$
44	43	eqeq2d	$⊢ z = x + 1 \to (y = F (z) \leftrightarrow y = F (x + 1))$
45	44	adantl	$⊢ (N \in ℕ_{0} \land z = x + 1) \to (y = F (z) \leftrightarrow y = F (x + 1))$
46	19 42 45	rexxfrd	$⊢ N \in ℕ_{0} \to (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1))$
47	46	adantr	$⊢ (N \in ℕ_{0} \land \|F\| = N) \to (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1))$
48		oveq2	$⊢ \|F\| = N \to (0 ..^\|F\|) = (0 ..^N)$
49	48	rexeqdv	$⊢ \|F\| = N \to (\exists x \in (0 ..^\|F\|) y = F (x + 1) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1))$
50	49	bibi2d	$⊢ \|F\| = N \to ((\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^\|F\|) y = F (x + 1)) \leftrightarrow (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1)))$
51	50	adantl	$⊢ (N \in ℕ_{0} \land \|F\| = N) \to ((\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^\|F\|) y = F (x + 1)) \leftrightarrow (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1)))$
52	47 51	mpbird	$⊢ (N \in ℕ_{0} \land \|F\| = N) \to (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^\|F\|) y = F (x + 1))$
53	18 52	syldan	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^\|F\|) y = F (x + 1))$
54	53	abbidv	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \{y \| \exists z \in (1 \dots N) y = F (z)\} = \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\}$
55	54	eqeq1d	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (\{y \| \exists z \in (1 \dots N) y = F (z)\} = dom E \leftrightarrow \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E)$
56	55	biimpcd	$⊢ \{y \| \exists z \in (1 \dots N) y = F (z)\} = dom E \to ((N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E)$
57	14 56	biimtrdi	$⊢ ran F = dom E \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \to ((N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E))$
58	57	com23	$⊢ ran F = dom E \to ((N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E))$
59	58	adantl	$⊢ (F Fn (1 \dots N) \land ran F = dom E) \to ((N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E))$
60	11 59	mpcom	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E)$
61	9 60	mpd	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E$
62	5 61	eqtrid	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to ran G = dom E$
63		dffo2	$⊢ G : (0 ..^\|F\|) \underset{onto}{⟶} dom E \leftrightarrow (G : (0 ..^\|F\|) ⟶ dom E \land ran G = dom E)$
64	4 62 63	sylanbrc	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to G : (0 ..^\|F\|) \underset{onto}{⟶} dom E$

Metamath Proof Explorer

Theorem fargshiftfo

Proof