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
|
syl6bir |
|- ( ( # ` 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 ) |