Metamath Proof Explorer

Theorem gsumval3eu

Description: The group sum as defined in gsumval3a is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014)

Ref Expression
Hypotheses gsumval3.b 
|- B = ( Base ` G )
gsumval3.0 
|- .0. = ( 0g ` G )
gsumval3.p 
|- .+ = ( +g ` G )
gsumval3.z 
|- Z = ( Cntz ` G )
gsumval3.g 
|- ( ph -> G e. Mnd )
gsumval3.a 
|- ( ph -> A e. V )
gsumval3.f 
|- ( ph -> F : A --> B )
gsumval3.c 
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumval3a.t 
|- ( ph -> W e. Fin )
gsumval3a.n 
|- ( ph -> W =/= (/) )
gsumval3a.s 
|- ( ph -> W C_ A )
Assertion gsumval3eu 
|- ( ph -> E! x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumval3.b 
 |-  B = ( Base ` G )
2 gsumval3.0 
 |-  .0. = ( 0g ` G )
3 gsumval3.p 
 |-  .+ = ( +g ` G )
4 gsumval3.z 
 |-  Z = ( Cntz ` G )
5 gsumval3.g 
 |-  ( ph -> G e. Mnd )
6 gsumval3.a 
 |-  ( ph -> A e. V )
7 gsumval3.f 
 |-  ( ph -> F : A --> B )
8 gsumval3.c 
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
9 gsumval3a.t 
 |-  ( ph -> W e. Fin )
10 gsumval3a.n 
 |-  ( ph -> W =/= (/) )
11 gsumval3a.s 
 |-  ( ph -> W C_ A )
12 10 neneqd 
 |-  ( ph -> -. W = (/) )
13 fz1f1o 
 |-  ( W e. Fin -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
14 9 13 syl 
 |-  ( ph -> ( W = (/) \/ ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
15 14 ord 
 |-  ( ph -> ( -. W = (/) -> ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) )
16 12 15 mpd 
 |-  ( ph -> ( ( # ` W ) e. NN /\ E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
17 16 simprd 
 |-  ( ph -> E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
18 excom 
 |-  ( E. x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> E. f E. x ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) )
19 exancom 
 |-  ( E. x ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> E. x ( x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
20 fvex 
 |-  ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) e. _V
21 biidd 
 |-  ( x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
22 20 21 ceqsexv 
 |-  ( E. x ( x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
23 19 22 bitri 
 |-  ( E. x ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
24 23 exbii 
 |-  ( E. f E. x ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
25 18 24 bitri 
 |-  ( E. x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> E. f f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
26 17 25 sylibr 
 |-  ( ph -> E. x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) )
27 exdistrv 
 |-  ( E. f E. g ( ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) /\ ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) <-> ( E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) /\ E. g ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) )
28 an4 
 |-  ( ( ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) /\ ( x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) <-> ( ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) /\ ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) )
29 5 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> G e. Mnd )
30 1 3 mndcl 
 |-  ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
31 30 3expb 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
32 29 31 sylan 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
33 8 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran F C_ ( Z ` ran F ) )
34 33 sselda 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ran F ) -> x e. ( Z ` ran F ) )
35 34 adantrr 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. ran F /\ y e. ran F ) ) -> x e. ( Z ` ran F ) )
36 simprr 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. ran F /\ y e. ran F ) ) -> y e. ran F )
37 3 4 cntzi 
 |-  ( ( x e. ( Z ` ran F ) /\ y e. ran F ) -> ( x .+ y ) = ( y .+ x ) )
38 35 36 37 syl2anc 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. ran F /\ y e. ran F ) ) -> ( x .+ y ) = ( y .+ x ) )
39 1 3 mndass 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
40 29 39 sylan 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
41 16 simpld 
 |-  ( ph -> ( # ` W ) e. NN )
42 41 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. NN )
43 nnuz 
 |-  NN = ( ZZ>= ` 1 )
44 42 43 eleqtrdi 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( # ` W ) e. ( ZZ>= ` 1 ) )
45 7 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F : A --> B )
46 45 frnd 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ran F C_ B )
47 simprr 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> g : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
48 f1ocnv 
 |-  ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> `' g : W -1-1-onto-> ( 1 ... ( # ` W ) ) )
49 47 48 syl 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> `' g : W -1-1-onto-> ( 1 ... ( # ` W ) ) )
50 simprl 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W )
51 f1oco 
 |-  ( ( `' g : W -1-1-onto-> ( 1 ... ( # ` W ) ) /\ f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) -> ( `' g o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( 1 ... ( # ` W ) ) )
52 49 50 51 syl2anc 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( `' g o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( 1 ... ( # ` W ) ) )
53 f1of 
 |-  ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> g : ( 1 ... ( # ` W ) ) --> W )
54 47 53 syl 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> g : ( 1 ... ( # ` W ) ) --> W )
55 fvco3 
 |-  ( ( g : ( 1 ... ( # ` W ) ) --> W /\ x e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. g ) ` x ) = ( F ` ( g ` x ) ) )
56 54 55 sylan 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. g ) ` x ) = ( F ` ( g ` x ) ) )
57 45 ffnd 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> F Fn A )
58 11 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> W C_ A )
59 54 58 fssd 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> g : ( 1 ... ( # ` W ) ) --> A )
60 59 ffvelrnda 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( 1 ... ( # ` W ) ) ) -> ( g ` x ) e. A )
61 fnfvelrn 
 |-  ( ( F Fn A /\ ( g ` x ) e. A ) -> ( F ` ( g ` x ) ) e. ran F )
62 57 60 61 syl2an2r 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( 1 ... ( # ` W ) ) ) -> ( F ` ( g ` x ) ) e. ran F )
63 56 62 eqeltrd 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ x e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. g ) ` x ) e. ran F )
64 f1of 
 |-  ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W -> f : ( 1 ... ( # ` W ) ) --> W )
65 50 64 syl 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> f : ( 1 ... ( # ` W ) ) --> W )
66 fvco3 
 |-  ( ( f : ( 1 ... ( # ` W ) ) --> W /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( `' g o. f ) ` k ) = ( `' g ` ( f ` k ) ) )
67 65 66 sylan 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( `' g o. f ) ` k ) = ( `' g ` ( f ` k ) ) )
68 67 fveq2d 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( g ` ( ( `' g o. f ) ` k ) ) = ( g ` ( `' g ` ( f ` k ) ) ) )
69 65 ffvelrnda 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( f ` k ) e. W )
70 f1ocnvfv2 
 |-  ( ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ ( f ` k ) e. W ) -> ( g ` ( `' g ` ( f ` k ) ) ) = ( f ` k ) )
71 47 69 70 syl2an2r 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( g ` ( `' g ` ( f ` k ) ) ) = ( f ` k ) )
72 68 71 eqtr2d 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( f ` k ) = ( g ` ( ( `' g o. f ) ` k ) ) )
73 72 fveq2d 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( F ` ( f ` k ) ) = ( F ` ( g ` ( ( `' g o. f ) ` k ) ) ) )
74 fvco3 
 |-  ( ( f : ( 1 ... ( # ` W ) ) --> W /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) = ( F ` ( f ` k ) ) )
75 65 74 sylan 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) = ( F ` ( f ` k ) ) )
76 f1of 
 |-  ( ( `' g o. f ) : ( 1 ... ( # ` W ) ) -1-1-onto-> ( 1 ... ( # ` W ) ) -> ( `' g o. f ) : ( 1 ... ( # ` W ) ) --> ( 1 ... ( # ` W ) ) )
77 52 76 syl 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( `' g o. f ) : ( 1 ... ( # ` W ) ) --> ( 1 ... ( # ` W ) ) )
78 77 ffvelrnda 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( `' g o. f ) ` k ) e. ( 1 ... ( # ` W ) ) )
79 fvco3 
 |-  ( ( g : ( 1 ... ( # ` W ) ) --> A /\ ( ( `' g o. f ) ` k ) e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. g ) ` ( ( `' g o. f ) ` k ) ) = ( F ` ( g ` ( ( `' g o. f ) ` k ) ) ) )
80 59 78 79 syl2an2r 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. g ) ` ( ( `' g o. f ) ` k ) ) = ( F ` ( g ` ( ( `' g o. f ) ` k ) ) ) )
81 73 75 80 3eqtr4d 
 |-  ( ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) /\ k e. ( 1 ... ( # ` W ) ) ) -> ( ( F o. f ) ` k ) = ( ( F o. g ) ` ( ( `' g o. f ) ` k ) ) )
82 32 38 40 44 46 52 63 81 seqf1o 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) )
83 eqeq12 
 |-  ( ( x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) -> ( x = y <-> ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) )
84 82 83 syl5ibrcom 
 |-  ( ( ph /\ ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) -> ( ( x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) -> x = y ) )
85 84 expimpd 
 |-  ( ph -> ( ( ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) /\ ( x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) -> x = y ) )
86 28 85 syl5bir 
 |-  ( ph -> ( ( ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) /\ ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) -> x = y ) )
87 86 exlimdvv 
 |-  ( ph -> ( E. f E. g ( ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) /\ ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) -> x = y ) )
88 27 87 syl5bir 
 |-  ( ph -> ( ( E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) /\ E. g ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) -> x = y ) )
89 88 alrimivv 
 |-  ( ph -> A. x A. y ( ( E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) /\ E. g ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) -> x = y ) )
90 eqeq1 
 |-  ( x = y -> ( x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) <-> y = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) )
91 90 anbi2d 
 |-  ( x = y -> ( ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )
92 91 exbidv 
 |-  ( x = y -> ( E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )
93 f1oeq1 
 |-  ( f = g -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W <-> g : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
94 coeq2 
 |-  ( f = g -> ( F o. f ) = ( F o. g ) )
95 94 seqeq3d 
 |-  ( f = g -> seq 1 ( .+ , ( F o. f ) ) = seq 1 ( .+ , ( F o. g ) ) )
96 95 fveq1d 
 |-  ( f = g -> ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) )
97 96 eqeq2d 
 |-  ( f = g -> ( y = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) <-> y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) )
98 93 97 anbi12d 
 |-  ( f = g -> ( ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) )
99 98 cbvexvw 
 |-  ( E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> E. g ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) )
100 92 99 bitrdi 
 |-  ( x = y -> ( E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> E. g ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) )
101 100 eu4 
 |-  ( E! x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) <-> ( E. x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) /\ A. x A. y ( ( E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) /\ E. g ( g : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ y = ( seq 1 ( .+ , ( F o. g ) ) ` ( # ` W ) ) ) ) -> x = y ) ) )
102 26 89 101 sylanbrc 
 |-  ( ph -> E! x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) )