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 e. ( 0 ..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )
Assertion fargshiftfo 
|- ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> G : ( 0 ..^ ( # ` F ) ) -onto-> dom E )

Proof

Step Hyp Ref Expression
1 fargshift.g 
 |-  G = ( x e. ( 0 ..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )
2 fof 
 |-  ( F : ( 1 ... N ) -onto-> dom E -> F : ( 1 ... N ) --> dom E )
3 1 fargshiftf 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> G : ( 0 ..^ ( # ` F ) ) --> dom E )
4 2 3 sylan2 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> G : ( 0 ..^ ( # ` F ) ) --> dom E )
5 1 rnmpt 
 |-  ran G = { y | E. x e. ( 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 | E. z e. ( 1 ... N ) y = ( F ` z ) } )
8 6 7 syl 
 |-  ( F : ( 1 ... N ) -onto-> dom E -> ran F = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } )
9 8 adantl 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ran F = { y | E. z e. ( 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 e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ( F Fn ( 1 ... N ) /\ ran F = dom E ) )
13 eqeq1 
 |-  ( ran F = dom E -> ( ran F = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } <-> dom E = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } ) )
14 eqcom 
 |-  ( dom E = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } <-> { y | E. z e. ( 1 ... N ) y = ( F ` z ) } = dom E )
15 13 14 bitrdi 
 |-  ( ran F = dom E -> ( ran F = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } <-> { y | E. z e. ( 1 ... N ) y = ( F ` z ) } = dom E ) )
16 ffn 
 |-  ( F : ( 1 ... N ) --> dom E -> F Fn ( 1 ... N ) )
17 fseq1hash 
 |-  ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( # ` F ) = N )
18 16 17 sylan2 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( # ` F ) = N )
19 2 18 sylan2 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ( # ` F ) = N )
20 fz0add1fz1 
 |-  ( ( N e. NN0 /\ x e. ( 0 ..^ N ) ) -> ( x + 1 ) e. ( 1 ... N ) )
21 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
22 fzval3 
 |-  ( N e. ZZ -> ( 1 ... N ) = ( 1 ..^ ( N + 1 ) ) )
23 21 22 syl 
 |-  ( N e. NN0 -> ( 1 ... N ) = ( 1 ..^ ( N + 1 ) ) )
24 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
25 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
26 24 25 addcomd 
 |-  ( N e. NN0 -> ( N + 1 ) = ( 1 + N ) )
27 26 oveq2d 
 |-  ( N e. NN0 -> ( 1 ..^ ( N + 1 ) ) = ( 1 ..^ ( 1 + N ) ) )
28 23 27 eqtrd 
 |-  ( N e. NN0 -> ( 1 ... N ) = ( 1 ..^ ( 1 + N ) ) )
29 28 eleq2d 
 |-  ( N e. NN0 -> ( z e. ( 1 ... N ) <-> z e. ( 1 ..^ ( 1 + N ) ) ) )
30 29 biimpa 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> z e. ( 1 ..^ ( 1 + N ) ) )
31 21 adantr 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> N e. ZZ )
32 fzosubel3 
 |-  ( ( z e. ( 1 ..^ ( 1 + N ) ) /\ N e. ZZ ) -> ( z - 1 ) e. ( 0 ..^ N ) )
33 30 31 32 syl2anc 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> ( z - 1 ) e. ( 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 e. NN0 /\ z e. ( 1 ... N ) ) /\ x = ( z - 1 ) ) -> ( z = ( x + 1 ) <-> z = ( ( z - 1 ) + 1 ) ) )
37 elfzelz 
 |-  ( z e. ( 1 ... N ) -> z e. ZZ )
38 37 zcnd 
 |-  ( z e. ( 1 ... N ) -> z e. CC )
39 38 adantl 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> z e. CC )
40 1cnd 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> 1 e. CC )
41 39 40 npcand 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> ( ( z - 1 ) + 1 ) = z )
42 41 eqcomd 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> z = ( ( z - 1 ) + 1 ) )
43 33 36 42 rspcedvd 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> E. x e. ( 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 e. NN0 /\ z = ( x + 1 ) ) -> ( y = ( F ` z ) <-> y = ( F ` ( x + 1 ) ) ) )
47 20 43 46 rexxfrd 
 |-  ( N e. NN0 -> ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ N ) y = ( F ` ( x + 1 ) ) ) )
48 47 adantr 
 |-  ( ( N e. NN0 /\ ( # ` F ) = N ) -> ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ N ) y = ( F ` ( x + 1 ) ) ) )
49 oveq2 
 |-  ( ( # ` F ) = N -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N ) )
50 49 rexeqdv 
 |-  ( ( # ` F ) = N -> ( E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) <-> E. x e. ( 0 ..^ N ) y = ( F ` ( x + 1 ) ) ) )
51 50 bibi2d 
 |-  ( ( # ` F ) = N -> ( ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) ) <-> ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ N ) y = ( F ` ( x + 1 ) ) ) ) )
52 51 adantl 
 |-  ( ( N e. NN0 /\ ( # ` F ) = N ) -> ( ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) ) <-> ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ N ) y = ( F ` ( x + 1 ) ) ) ) )
53 48 52 mpbird 
 |-  ( ( N e. NN0 /\ ( # ` F ) = N ) -> ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) ) )
54 19 53 syldan 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) ) )
55 54 abbidv 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> { y | E. z e. ( 1 ... N ) y = ( F ` z ) } = { y | E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) } )
56 55 eqeq1d 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ( { y | E. z e. ( 1 ... N ) y = ( F ` z ) } = dom E <-> { y | E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) } = dom E ) )
57 56 biimpcd 
 |-  ( { y | E. z e. ( 1 ... N ) y = ( F ` z ) } = dom E -> ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> { y | E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) } = dom E ) )
58 15 57 syl6bi 
 |-  ( ran F = dom E -> ( ran F = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } -> ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> { y | E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) } = dom E ) ) )
59 58 com23 
 |-  ( ran F = dom E -> ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ( ran F = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } -> { y | E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) } = dom E ) ) )
60 59 adantl 
 |-  ( ( F Fn ( 1 ... N ) /\ ran F = dom E ) -> ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ( ran F = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } -> { y | E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) } = dom E ) ) )
61 12 60 mpcom 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ( ran F = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } -> { y | E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) } = dom E ) )
62 9 61 mpd 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> { y | E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) } = dom E )
63 5 62 syl5eq 
 |-  ( ( N e. NN0 /\ 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 e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> G : ( 0 ..^ ( # ` F ) ) -onto-> dom E )