Metamath Proof Explorer

Theorem fargshiftf1

Description: If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017)

Ref Expression
Hypothesis fargshift.g 
|- G = ( x e. ( 0 ..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )
Assertion fargshiftf1 
|- ( ( N e. NN0 /\ F : ( 1 ... N ) -1-1-> dom E ) -> G : ( 0 ..^ ( # ` F ) ) -1-1-> dom E )

Proof

Step Hyp Ref Expression
1 fargshift.g 
 |-  G = ( x e. ( 0 ..^ ( # ` F ) ) |-> ( F ` ( x + 1 ) ) )
2 f1f 
 |-  ( F : ( 1 ... N ) -1-1-> 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 ) -1-1-> dom E ) -> G : ( 0 ..^ ( # ` F ) ) --> dom E )
5 ffn 
 |-  ( F : ( 1 ... N ) --> dom E -> F Fn ( 1 ... N ) )
6 fseq1hash 
 |-  ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( # ` F ) = N )
7 5 6 sylan2 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) --> dom E ) -> ( # ` F ) = N )
8 2 7 sylan2 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -1-1-> dom E ) -> ( # ` F ) = N )
9 eleq1 
 |-  ( ( # ` F ) = N -> ( ( # ` F ) e. NN0 <-> N e. NN0 ) )
10 oveq2 
 |-  ( ( # ` F ) = N -> ( 1 ... ( # ` F ) ) = ( 1 ... N ) )
11 f1eq2 
 |-  ( ( 1 ... ( # ` F ) ) = ( 1 ... N ) -> ( F : ( 1 ... ( # ` F ) ) -1-1-> dom E <-> F : ( 1 ... N ) -1-1-> dom E ) )
12 10 11 syl 
 |-  ( ( # ` F ) = N -> ( F : ( 1 ... ( # ` F ) ) -1-1-> dom E <-> F : ( 1 ... N ) -1-1-> dom E ) )
13 9 12 anbi12d 
 |-  ( ( # ` F ) = N -> ( ( ( # ` F ) e. NN0 /\ F : ( 1 ... ( # ` F ) ) -1-1-> dom E ) <-> ( N e. NN0 /\ F : ( 1 ... N ) -1-1-> dom E ) ) )
14 dff13 
 |-  ( F : ( 1 ... ( # ` F ) ) -1-1-> dom E <-> ( F : ( 1 ... ( # ` F ) ) --> dom E /\ A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) ) )
15 fz0add1fz1 
 |-  ( ( ( # ` F ) e. NN0 /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( y + 1 ) e. ( 1 ... ( # ` F ) ) )
16 fz0add1fz1 
 |-  ( ( ( # ` F ) e. NN0 /\ z e. ( 0 ..^ ( # ` F ) ) ) -> ( z + 1 ) e. ( 1 ... ( # ` F ) ) )
17 15 16 anim12dan 
 |-  ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) )
18 fveq2 
 |-  ( k = ( y + 1 ) -> ( F ` k ) = ( F ` ( y + 1 ) ) )
19 18 eqeq1d 
 |-  ( k = ( y + 1 ) -> ( ( F ` k ) = ( F ` l ) <-> ( F ` ( y + 1 ) ) = ( F ` l ) ) )
20 eqeq1 
 |-  ( k = ( y + 1 ) -> ( k = l <-> ( y + 1 ) = l ) )
21 19 20 imbi12d 
 |-  ( k = ( y + 1 ) -> ( ( ( F ` k ) = ( F ` l ) -> k = l ) <-> ( ( F ` ( y + 1 ) ) = ( F ` l ) -> ( y + 1 ) = l ) ) )
22 fveq2 
 |-  ( l = ( z + 1 ) -> ( F ` l ) = ( F ` ( z + 1 ) ) )
23 22 eqeq2d 
 |-  ( l = ( z + 1 ) -> ( ( F ` ( y + 1 ) ) = ( F ` l ) <-> ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) ) )
24 eqeq2 
 |-  ( l = ( z + 1 ) -> ( ( y + 1 ) = l <-> ( y + 1 ) = ( z + 1 ) ) )
25 23 24 imbi12d 
 |-  ( l = ( z + 1 ) -> ( ( ( F ` ( y + 1 ) ) = ( F ` l ) -> ( y + 1 ) = l ) <-> ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> ( y + 1 ) = ( z + 1 ) ) ) )
26 21 25 rspc2v 
 |-  ( ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) -> ( A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) -> ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> ( y + 1 ) = ( z + 1 ) ) ) )
27 26 adantl 
 |-  ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) -> ( A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) -> ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> ( y + 1 ) = ( z + 1 ) ) ) )
28 1 fargshiftfv 
 |-  ( ( ( # ` F ) e. NN0 /\ F : ( 1 ... ( # ` F ) ) --> dom E ) -> ( y e. ( 0 ..^ ( # ` F ) ) -> ( G ` y ) = ( F ` ( y + 1 ) ) ) )
29 28 expcom 
 |-  ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( ( # ` F ) e. NN0 -> ( y e. ( 0 ..^ ( # ` F ) ) -> ( G ` y ) = ( F ` ( y + 1 ) ) ) ) )
30 29 com13 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> ( ( # ` F ) e. NN0 -> ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( G ` y ) = ( F ` ( y + 1 ) ) ) ) )
31 30 adantr 
 |-  ( ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) -> ( ( # ` F ) e. NN0 -> ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( G ` y ) = ( F ` ( y + 1 ) ) ) ) )
32 31 impcom 
 |-  ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( G ` y ) = ( F ` ( y + 1 ) ) ) )
33 32 impcom 
 |-  ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) -> ( G ` y ) = ( F ` ( y + 1 ) ) )
34 1 fargshiftfv 
 |-  ( ( ( # ` F ) e. NN0 /\ F : ( 1 ... ( # ` F ) ) --> dom E ) -> ( z e. ( 0 ..^ ( # ` F ) ) -> ( G ` z ) = ( F ` ( z + 1 ) ) ) )
35 34 expcom 
 |-  ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( ( # ` F ) e. NN0 -> ( z e. ( 0 ..^ ( # ` F ) ) -> ( G ` z ) = ( F ` ( z + 1 ) ) ) ) )
36 35 com13 
 |-  ( z e. ( 0 ..^ ( # ` F ) ) -> ( ( # ` F ) e. NN0 -> ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( G ` z ) = ( F ` ( z + 1 ) ) ) ) )
37 36 adantl 
 |-  ( ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) -> ( ( # ` F ) e. NN0 -> ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( G ` z ) = ( F ` ( z + 1 ) ) ) ) )
38 37 impcom 
 |-  ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( G ` z ) = ( F ` ( z + 1 ) ) ) )
39 38 impcom 
 |-  ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) -> ( G ` z ) = ( F ` ( z + 1 ) ) )
40 33 39 eqeq12d 
 |-  ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) -> ( ( G ` y ) = ( G ` z ) <-> ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) ) )
41 40 adantr 
 |-  ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) -> ( ( G ` y ) = ( G ` z ) <-> ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) ) )
42 41 adantr 
 |-  ( ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) /\ ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> ( y + 1 ) = ( z + 1 ) ) ) -> ( ( G ` y ) = ( G ` z ) <-> ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) ) )
43 elfzoelz 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> y e. ZZ )
44 43 zcnd 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> y e. CC )
45 44 adantr 
 |-  ( ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) -> y e. CC )
46 45 adantl 
 |-  ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> y e. CC )
47 elfzoelz 
 |-  ( z e. ( 0 ..^ ( # ` F ) ) -> z e. ZZ )
48 47 zcnd 
 |-  ( z e. ( 0 ..^ ( # ` F ) ) -> z e. CC )
49 48 adantl 
 |-  ( ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) -> z e. CC )
50 49 adantl 
 |-  ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> z e. CC )
51 1cnd 
 |-  ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> 1 e. CC )
52 46 50 51 3jca 
 |-  ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> ( y e. CC /\ z e. CC /\ 1 e. CC ) )
53 52 adantl 
 |-  ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) -> ( y e. CC /\ z e. CC /\ 1 e. CC ) )
54 53 adantr 
 |-  ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) -> ( y e. CC /\ z e. CC /\ 1 e. CC ) )
55 addcan2 
 |-  ( ( y e. CC /\ z e. CC /\ 1 e. CC ) -> ( ( y + 1 ) = ( z + 1 ) <-> y = z ) )
56 54 55 syl 
 |-  ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) -> ( ( y + 1 ) = ( z + 1 ) <-> y = z ) )
57 56 imbi2d 
 |-  ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) -> ( ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> ( y + 1 ) = ( z + 1 ) ) <-> ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> y = z ) ) )
58 57 biimpa 
 |-  ( ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) /\ ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> ( y + 1 ) = ( z + 1 ) ) ) -> ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> y = z ) )
59 42 58 sylbid 
 |-  ( ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) /\ ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> ( y + 1 ) = ( z + 1 ) ) ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) )
60 59 ex 
 |-  ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) -> ( ( ( F ` ( y + 1 ) ) = ( F ` ( z + 1 ) ) -> ( y + 1 ) = ( z + 1 ) ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) ) )
61 27 60 syld 
 |-  ( ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) ) /\ ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) ) -> ( A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) ) )
62 61 exp31 
 |-  ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) -> ( A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) ) ) ) )
63 62 com24 
 |-  ( F : ( 1 ... ( # ` F ) ) --> dom E -> ( A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) -> ( ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) -> ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) ) ) ) )
64 63 imp 
 |-  ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) ) -> ( ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) -> ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) ) ) )
65 64 com13 
 |-  ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( y + 1 ) e. ( 1 ... ( # ` F ) ) /\ ( z + 1 ) e. ( 1 ... ( # ` F ) ) ) -> ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) ) ) )
66 17 65 mpd 
 |-  ( ( ( # ` F ) e. NN0 /\ ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) ) )
67 66 expcom 
 |-  ( ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) -> ( ( # ` F ) e. NN0 -> ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) ) ) )
68 67 com13 
 |-  ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) ) -> ( ( # ` F ) e. NN0 -> ( ( y e. ( 0 ..^ ( # ` F ) ) /\ z e. ( 0 ..^ ( # ` F ) ) ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) ) ) )
69 68 ralrimdvv 
 |-  ( ( F : ( 1 ... ( # ` F ) ) --> dom E /\ A. k e. ( 1 ... ( # ` F ) ) A. l e. ( 1 ... ( # ` F ) ) ( ( F ` k ) = ( F ` l ) -> k = l ) ) -> ( ( # ` F ) e. NN0 -> A. y e. ( 0 ..^ ( # ` F ) ) A. z e. ( 0 ..^ ( # ` F ) ) ( ( G ` y ) = ( G ` z ) -> y = z ) ) )
70 14 69 sylbi 
 |-  ( F : ( 1 ... ( # ` F ) ) -1-1-> dom E -> ( ( # ` F ) e. NN0 -> A. y e. ( 0 ..^ ( # ` F ) ) A. z e. ( 0 ..^ ( # ` F ) ) ( ( G ` y ) = ( G ` z ) -> y = z ) ) )
71 70 impcom 
 |-  ( ( ( # ` F ) e. NN0 /\ F : ( 1 ... ( # ` F ) ) -1-1-> dom E ) -> A. y e. ( 0 ..^ ( # ` F ) ) A. z e. ( 0 ..^ ( # ` F ) ) ( ( G ` y ) = ( G ` z ) -> y = z ) )
72 13 71 biimtrrdi 
 |-  ( ( # ` F ) = N -> ( ( N e. NN0 /\ F : ( 1 ... N ) -1-1-> dom E ) -> A. y e. ( 0 ..^ ( # ` F ) ) A. z e. ( 0 ..^ ( # ` F ) ) ( ( G ` y ) = ( G ` z ) -> y = z ) ) )
73 8 72 mpcom 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -1-1-> dom E ) -> A. y e. ( 0 ..^ ( # ` F ) ) A. z e. ( 0 ..^ ( # ` F ) ) ( ( G ` y ) = ( G ` z ) -> y = z ) )
74 dff13 
 |-  ( G : ( 0 ..^ ( # ` F ) ) -1-1-> dom E <-> ( G : ( 0 ..^ ( # ` F ) ) --> dom E /\ A. y e. ( 0 ..^ ( # ` F ) ) A. z e. ( 0 ..^ ( # ` F ) ) ( ( G ` y ) = ( G ` z ) -> y = z ) ) )
75 4 73 74 sylanbrc 
 |-  ( ( N e. NN0 /\ F : ( 1 ... N ) -1-1-> dom E ) -> G : ( 0 ..^ ( # ` F ) ) -1-1-> dom E )