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 G = x 0 ..^ F F x + 1
Assertion fargshiftfo N 0 F : 1 N onto dom E G : 0 ..^ F onto dom E

Proof

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