Metamath Proof Explorer

Theorem 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 ⊢ 𝐺 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↦ ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
Assertion fargshiftfo ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐸 )

Proof

Step Hyp Ref Expression
1 fargshift.g ⊢ 𝐺 = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↦ ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
2 fof ⊢ ( 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 → 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 )
3 1 fargshiftf ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 )
4 2 3 sylan2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 )
5 1 rnmpt ⊢ ran 𝐺 = { 𝑦 ∣ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) }
6 fofn ⊢ ( 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 → 𝐹 Fn ( 1 ... 𝑁 ) )
7 fnrnfv ⊢ ( 𝐹 Fn ( 1 ... 𝑁 ) → ran 𝐹 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } )
8 6 7 syl ⊢ ( 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } )
9 8 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → ran 𝐹 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } )
10 df-fo ⊢ ( 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ↔ ( 𝐹 Fn ( 1 ... 𝑁 ) ∧ ran 𝐹 = dom 𝐸 ) )
11 10 biimpi ⊢ ( 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 → ( 𝐹 Fn ( 1 ... 𝑁 ) ∧ ran 𝐹 = dom 𝐸 ) )
12 11 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → ( 𝐹 Fn ( 1 ... 𝑁 ) ∧ ran 𝐹 = dom 𝐸 ) )
13 eqeq1 ⊢ ( ran 𝐹 = dom 𝐸 → ( ran 𝐹 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } ↔ dom 𝐸 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } ) )
14 eqcom ⊢ ( dom 𝐸 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } ↔ { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } = dom 𝐸 )
15 13 14 bitrdi ⊢ ( ran 𝐹 = dom 𝐸 → ( ran 𝐹 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } ↔ { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } = dom 𝐸 ) )
16 ffn ⊢ ( 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 → 𝐹 Fn ( 1 ... 𝑁 ) )
17 fseq1hash ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 Fn ( 1 ... 𝑁 ) ) → ( ♯ ‘ 𝐹 ) = 𝑁 )
18 16 17 sylan2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ dom 𝐸 ) → ( ♯ ‘ 𝐹 ) = 𝑁 )
19 2 18 sylan2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → ( ♯ ‘ 𝐹 ) = 𝑁 )
20 fz0add1fz1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑥 + 1 ) ∈ ( 1 ... 𝑁 ) )
21 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
22 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 1 ... 𝑁 ) = ( 1 ..^ ( 𝑁 + 1 ) ) )
23 21 22 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) = ( 1 ..^ ( 𝑁 + 1 ) ) )
24 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
25 1cnd ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℂ )
26 24 25 addcomd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) = ( 1 + 𝑁 ) )
27 26 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ..^ ( 𝑁 + 1 ) ) = ( 1 ..^ ( 1 + 𝑁 ) ) )
28 23 27 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) = ( 1 ..^ ( 1 + 𝑁 ) ) )
29 28 eleq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑧 ∈ ( 1 ... 𝑁 ) ↔ 𝑧 ∈ ( 1 ..^ ( 1 + 𝑁 ) ) ) )
30 29 biimpa ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → 𝑧 ∈ ( 1 ..^ ( 1 + 𝑁 ) ) )
31 21 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
32 fzosubel3 ⊢ ( ( 𝑧 ∈ ( 1 ..^ ( 1 + 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → ( 𝑧 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
33 30 31 32 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
34 oveq1 ⊢ ( 𝑥 = ( 𝑧 − 1 ) → ( 𝑥 + 1 ) = ( ( 𝑧 − 1 ) + 1 ) )
35 34 eqeq2d ⊢ ( 𝑥 = ( 𝑧 − 1 ) → ( 𝑧 = ( 𝑥 + 1 ) ↔ 𝑧 = ( ( 𝑧 − 1 ) + 1 ) ) )
36 35 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑥 = ( 𝑧 − 1 ) ) → ( 𝑧 = ( 𝑥 + 1 ) ↔ 𝑧 = ( ( 𝑧 − 1 ) + 1 ) ) )
37 elfzelz ⊢ ( 𝑧 ∈ ( 1 ... 𝑁 ) → 𝑧 ∈ ℤ )
38 37 zcnd ⊢ ( 𝑧 ∈ ( 1 ... 𝑁 ) → 𝑧 ∈ ℂ )
39 38 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → 𝑧 ∈ ℂ )
40 1cnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℂ )
41 39 40 npcand ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑧 − 1 ) + 1 ) = 𝑧 )
42 41 eqcomd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → 𝑧 = ( ( 𝑧 − 1 ) + 1 ) )
43 33 36 42 rspcedvd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑧 = ( 𝑥 + 1 ) )
44 fveq2 ⊢ ( 𝑧 = ( 𝑥 + 1 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
45 44 eqeq2d ⊢ ( 𝑧 = ( 𝑥 + 1 ) → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
46 45 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 = ( 𝑥 + 1 ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
47 20 43 46 rexxfrd ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
48 47 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) → ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
49 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 ) )
50 49 rexeqdv ⊢ ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
51 50 bibi2d ⊢ ( ( ♯ ‘ 𝐹 ) = 𝑁 → ( ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ↔ ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ) )
52 51 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) → ( ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ↔ ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ) )
53 48 52 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) = 𝑁 ) → ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
54 19 53 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → ( ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
55 54 abbidv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } = { 𝑦 ∣ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) } )
56 55 eqeq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → ( { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } = dom 𝐸 ↔ { 𝑦 ∣ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) } = dom 𝐸 ) )
57 56 biimpcd ⊢ ( { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } = dom 𝐸 → ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → { 𝑦 ∣ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) } = dom 𝐸 ) )
58 15 57 syl6bi ⊢ ( ran 𝐹 = dom 𝐸 → ( ran 𝐹 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } → ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → { 𝑦 ∣ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) } = dom 𝐸 ) ) )
59 58 com23 ⊢ ( ran 𝐹 = dom 𝐸 → ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → ( ran 𝐹 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } → { 𝑦 ∣ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) } = dom 𝐸 ) ) )
60 59 adantl ⊢ ( ( 𝐹 Fn ( 1 ... 𝑁 ) ∧ ran 𝐹 = dom 𝐸 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → ( ran 𝐹 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } → { 𝑦 ∣ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) } = dom 𝐸 ) ) )
61 12 60 mpcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → ( ran 𝐹 = { 𝑦 ∣ ∃ 𝑧 ∈ ( 1 ... 𝑁 ) 𝑦 = ( 𝐹 ‘ 𝑧 ) } → { 𝑦 ∣ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) } = dom 𝐸 ) )
62 9 61 mpd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → { 𝑦 ∣ ∃ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) 𝑦 = ( 𝐹 ‘ ( 𝑥 + 1 ) ) } = dom 𝐸 )
63 5 62 syl5eq ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → ran 𝐺 = dom 𝐸 )
64 dffo2 ⊢ ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐸 ↔ ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ∧ ran 𝐺 = dom 𝐸 ) )
65 4 63 64 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) –onto→ dom 𝐸 ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐸 )