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