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 bilani 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ( F Fn ( 1 ... N ) /\ ran F = dom E ) )
12 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 ) } ) )
13 eqcom 
 |-  ( dom E = { y | E. z e. ( 1 ... N ) y = ( F ` z ) } <-> { y | E. z e. ( 1 ... N ) y = ( F ` z ) } = dom E )
14 12 13 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 ) )
15 ffn 
 |-  ( F : ( 1 ... N ) --> dom E -> F Fn ( 1 ... N ) )
16 fseq1hash 
 |-  ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( # ` F ) = N )
17 15 16 sylan2 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( # ` F ) = N )
18 2 17 sylan2 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ( # ` F ) = N )
19 fz0add1fz1 
 |-  ( ( N e. NN0 /\ x e. ( 0 ..^ N ) ) -> ( x + 1 ) e. ( 1 ... N ) )
20 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
21 fzval3 
 |-  ( N e. ZZ -> ( 1 ... N ) = ( 1 ..^ ( N + 1 ) ) )
22 20 21 syl 
 |-  ( N e. NN0 -> ( 1 ... N ) = ( 1 ..^ ( N + 1 ) ) )
23 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
24 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
25 23 24 addcomd 
 |-  ( N e. NN0 -> ( N + 1 ) = ( 1 + N ) )
26 25 oveq2d 
 |-  ( N e. NN0 -> ( 1 ..^ ( N + 1 ) ) = ( 1 ..^ ( 1 + N ) ) )
27 22 26 eqtrd 
 |-  ( N e. NN0 -> ( 1 ... N ) = ( 1 ..^ ( 1 + N ) ) )
28 27 eleq2d 
 |-  ( N e. NN0 -> ( z e. ( 1 ... N ) <-> z e. ( 1 ..^ ( 1 + N ) ) ) )
29 28 biimpa 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> z e. ( 1 ..^ ( 1 + N ) ) )
30 20 adantr 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> N e. ZZ )
31 fzosubel3 
 |-  ( ( z e. ( 1 ..^ ( 1 + N ) ) /\ N e. ZZ ) -> ( z - 1 ) e. ( 0 ..^ N ) )
32 29 30 31 syl2anc 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> ( z - 1 ) e. ( 0 ..^ N ) )
33 oveq1 
 |-  ( x = ( z - 1 ) -> ( x + 1 ) = ( ( z - 1 ) + 1 ) )
34 33 eqeq2d 
 |-  ( x = ( z - 1 ) -> ( z = ( x + 1 ) <-> z = ( ( z - 1 ) + 1 ) ) )
35 34 adantl 
 |-  ( ( ( N e. NN0 /\ z e. ( 1 ... N ) ) /\ x = ( z - 1 ) ) -> ( z = ( x + 1 ) <-> z = ( ( z - 1 ) + 1 ) ) )
36 elfzelz 
 |-  ( z e. ( 1 ... N ) -> z e. ZZ )
37 36 zcnd 
 |-  ( z e. ( 1 ... N ) -> z e. CC )
38 37 adantl 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> z e. CC )
39 1cnd 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> 1 e. CC )
40 38 39 npcand 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> ( ( z - 1 ) + 1 ) = z )
41 40 eqcomd 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> z = ( ( z - 1 ) + 1 ) )
42 32 35 41 rspcedvd 
 |-  ( ( N e. NN0 /\ z e. ( 1 ... N ) ) -> E. x e. ( 0 ..^ N ) z = ( x + 1 ) )
43 fveq2 
 |-  ( z = ( x + 1 ) -> ( F ` z ) = ( F ` ( x + 1 ) ) )
44 43 eqeq2d 
 |-  ( z = ( x + 1 ) -> ( y = ( F ` z ) <-> y = ( F ` ( x + 1 ) ) ) )
45 44 adantl 
 |-  ( ( N e. NN0 /\ z = ( x + 1 ) ) -> ( y = ( F ` z ) <-> y = ( F ` ( x + 1 ) ) ) )
46 19 42 45 rexxfrd 
 |-  ( N e. NN0 -> ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ N ) y = ( F ` ( x + 1 ) ) ) )
47 46 adantr 
 |-  ( ( N e. NN0 /\ ( # ` F ) = N ) -> ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ N ) y = ( F ` ( x + 1 ) ) ) )
48 oveq2 
 |-  ( ( # ` F ) = N -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N ) )
49 48 rexeqdv 
 |-  ( ( # ` F ) = N -> ( E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) <-> E. x e. ( 0 ..^ N ) y = ( F ` ( x + 1 ) ) ) )
50 49 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 ) ) ) ) )
51 50 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 ) ) ) ) )
52 47 51 mpbird 
 |-  ( ( N e. NN0 /\ ( # ` F ) = N ) -> ( E. z e. ( 1 ... N ) y = ( F ` z ) <-> E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) ) )
53 18 52 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 ) ) ) )
54 53 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 ) ) } )
55 54 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 ) )
56 55 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 ) )
57 14 56 biimtrdi 
 |-  ( 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 ) ) )
58 57 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 ) ) )
59 58 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 ) ) )
60 11 59 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 ) )
61 9 60 mpd 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> { y | E. x e. ( 0 ..^ ( # ` F ) ) y = ( F ` ( x + 1 ) ) } = dom E )
62 5 61 eqtrid 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> ran G = dom E )
63 dffo2 
 |-  ( G : ( 0 ..^ ( # ` F ) ) -onto-> dom E <-> ( G : ( 0 ..^ ( # ` F ) ) --> dom E /\ ran G = dom E ) )
64 4 62 63 sylanbrc 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -onto-> dom E ) -> G : ( 0 ..^ ( # ` F ) ) -onto-> dom E )