Metamath Proof Explorer

Theorem prodmo

Description: A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
prodmo.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
prodmo.3 
|- G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
Assertion prodmo 
|- ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) )

Proof

Step Hyp Ref Expression
1 prodmo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
2 prodmo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 prodmo.3 
 |-  G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
4 3simpb 
 |-  ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) -> ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) )
5 4 reximi 
 |-  ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) -> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) )
6 3simpb 
 |-  ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) -> ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> z ) )
7 6 reximi 
 |-  ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) -> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> z ) )
8 fveq2 
 |-  ( m = w -> ( ZZ>= ` m ) = ( ZZ>= ` w ) )
9 8 sseq2d 
 |-  ( m = w -> ( A C_ ( ZZ>= ` m ) <-> A C_ ( ZZ>= ` w ) ) )
10 seqeq1 
 |-  ( m = w -> seq m ( x. , F ) = seq w ( x. , F ) )
11 10 breq1d 
 |-  ( m = w -> ( seq m ( x. , F ) ~~> z <-> seq w ( x. , F ) ~~> z ) )
12 9 11 anbi12d 
 |-  ( m = w -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> z ) <-> ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) )
13 12 cbvrexvw 
 |-  ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> z ) <-> E. w e. ZZ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) )
14 13 anbi2i 
 |-  ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> z ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ E. w e. ZZ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) )
15 reeanv 
 |-  ( E. m e. ZZ E. w e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ E. w e. ZZ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) )
16 14 15 bitr4i 
 |-  ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> z ) ) <-> E. m e. ZZ E. w e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) )
17 simprlr 
 |-  ( ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) -> seq m ( x. , F ) ~~> x )
18 17 adantl 
 |-  ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) -> seq m ( x. , F ) ~~> x )
19 2 adantlr 
 |-  ( ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) /\ k e. A ) -> B e. CC )
20 simprll 
 |-  ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) -> m e. ZZ )
21 simprlr 
 |-  ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) -> w e. ZZ )
22 simprll 
 |-  ( ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) -> A C_ ( ZZ>= ` m ) )
23 22 adantl 
 |-  ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) -> A C_ ( ZZ>= ` m ) )
24 simprrl 
 |-  ( ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) -> A C_ ( ZZ>= ` w ) )
25 24 adantl 
 |-  ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) -> A C_ ( ZZ>= ` w ) )
26 1 19 20 21 23 25 prodrb 
 |-  ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) -> ( seq m ( x. , F ) ~~> x <-> seq w ( x. , F ) ~~> x ) )
27 18 26 mpbid 
 |-  ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) -> seq w ( x. , F ) ~~> x )
28 simprrr 
 |-  ( ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) -> seq w ( x. , F ) ~~> z )
29 28 adantl 
 |-  ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) -> seq w ( x. , F ) ~~> z )
30 climuni 
 |-  ( ( seq w ( x. , F ) ~~> x /\ seq w ( x. , F ) ~~> z ) -> x = z )
31 27 29 30 syl2anc 
 |-  ( ( ph /\ ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) ) -> x = z )
32 31 expcom 
 |-  ( ( ( m e. ZZ /\ w e. ZZ ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) ) -> ( ph -> x = z ) )
33 32 ex 
 |-  ( ( m e. ZZ /\ w e. ZZ ) -> ( ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) -> ( ph -> x = z ) ) )
34 33 rexlimivv 
 |-  ( E. m e. ZZ E. w e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` w ) /\ seq w ( x. , F ) ~~> z ) ) -> ( ph -> x = z ) )
35 16 34 sylbi 
 |-  ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> x ) /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , F ) ~~> z ) ) -> ( ph -> x = z ) )
36 5 7 35 syl2an 
 |-  ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) ) -> ( ph -> x = z ) )
37 1 2 3 prodmolem2 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) -> z = x ) )
38 equcomi 
 |-  ( z = x -> x = z )
39 37 38 syl6 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )
40 39 expimpd 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) -> x = z ) )
41 40 com12 
 |-  ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) -> ( ph -> x = z ) )
42 41 ancoms 
 |-  ( ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) ) -> ( ph -> x = z ) )
43 1 2 3 prodmolem2 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )
44 43 expimpd 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) -> x = z ) )
45 44 com12 
 |-  ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) -> ( ph -> x = z ) )
46 reeanv 
 |-  ( E. m e. NN E. w e. NN ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. g ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) <-> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. w e. NN E. g ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) )
47 exdistrv 
 |-  ( E. f E. g ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) <-> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. g ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) )
48 47 2rexbii 
 |-  ( E. m e. NN E. w e. NN E. f E. g ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) <-> E. m e. NN E. w e. NN ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. g ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) )
49 oveq2 
 |-  ( m = w -> ( 1 ... m ) = ( 1 ... w ) )
50 49 f1oeq2d 
 |-  ( m = w -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... w ) -1-1-onto-> A ) )
51 fveq2 
 |-  ( m = w -> ( seq 1 ( x. , G ) ` m ) = ( seq 1 ( x. , G ) ` w ) )
52 51 eqeq2d 
 |-  ( m = w -> ( z = ( seq 1 ( x. , G ) ` m ) <-> z = ( seq 1 ( x. , G ) ` w ) ) )
53 50 52 anbi12d 
 |-  ( m = w -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) <-> ( f : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` w ) ) ) )
54 53 exbidv 
 |-  ( m = w -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) <-> E. f ( f : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` w ) ) ) )
55 f1oeq1 
 |-  ( f = g -> ( f : ( 1 ... w ) -1-1-onto-> A <-> g : ( 1 ... w ) -1-1-onto-> A ) )
56 fveq1 
 |-  ( f = g -> ( f ` j ) = ( g ` j ) )
57 56 csbeq1d 
 |-  ( f = g -> [_ ( f ` j ) / k ]_ B = [_ ( g ` j ) / k ]_ B )
58 57 mpteq2dv 
 |-  ( f = g -> ( j e. NN |-> [_ ( f ` j ) / k ]_ B ) = ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) )
59 3 58 eqtrid 
 |-  ( f = g -> G = ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) )
60 59 seqeq3d 
 |-  ( f = g -> seq 1 ( x. , G ) = seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) )
61 60 fveq1d 
 |-  ( f = g -> ( seq 1 ( x. , G ) ` w ) = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) )
62 61 eqeq2d 
 |-  ( f = g -> ( z = ( seq 1 ( x. , G ) ` w ) <-> z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) )
63 55 62 anbi12d 
 |-  ( f = g -> ( ( f : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` w ) ) <-> ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) )
64 63 cbvexvw 
 |-  ( E. f ( f : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` w ) ) <-> E. g ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) )
65 54 64 bitrdi 
 |-  ( m = w -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) <-> E. g ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) )
66 65 cbvrexvw 
 |-  ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) <-> E. w e. NN E. g ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) )
67 66 anbi2i 
 |-  ( ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) <-> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. w e. NN E. g ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) )
68 46 48 67 3bitr4i 
 |-  ( E. m e. NN E. w e. NN E. f E. g ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) <-> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) )
69 an4 
 |-  ( ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) <-> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... w ) -1-1-onto-> A ) /\ ( x = ( seq 1 ( x. , G ) ` m ) /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) )
70 2 ad4ant14 
 |-  ( ( ( ( ph /\ ( m e. NN /\ w e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... w ) -1-1-onto-> A ) ) /\ k e. A ) -> B e. CC )
71 fveq2 
 |-  ( j = a -> ( f ` j ) = ( f ` a ) )
72 71 csbeq1d 
 |-  ( j = a -> [_ ( f ` j ) / k ]_ B = [_ ( f ` a ) / k ]_ B )
73 72 cbvmptv 
 |-  ( j e. NN |-> [_ ( f ` j ) / k ]_ B ) = ( a e. NN |-> [_ ( f ` a ) / k ]_ B )
74 3 73 eqtri 
 |-  G = ( a e. NN |-> [_ ( f ` a ) / k ]_ B )
75 fveq2 
 |-  ( j = a -> ( g ` j ) = ( g ` a ) )
76 75 csbeq1d 
 |-  ( j = a -> [_ ( g ` j ) / k ]_ B = [_ ( g ` a ) / k ]_ B )
77 76 cbvmptv 
 |-  ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) = ( a e. NN |-> [_ ( g ` a ) / k ]_ B )
78 simplr 
 |-  ( ( ( ph /\ ( m e. NN /\ w e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... w ) -1-1-onto-> A ) ) -> ( m e. NN /\ w e. NN ) )
79 simprl 
 |-  ( ( ( ph /\ ( m e. NN /\ w e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... w ) -1-1-onto-> A ) ) -> f : ( 1 ... m ) -1-1-onto-> A )
80 simprr 
 |-  ( ( ( ph /\ ( m e. NN /\ w e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... w ) -1-1-onto-> A ) ) -> g : ( 1 ... w ) -1-1-onto-> A )
81 1 70 74 77 78 79 80 prodmolem3 
 |-  ( ( ( ph /\ ( m e. NN /\ w e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... w ) -1-1-onto-> A ) ) -> ( seq 1 ( x. , G ) ` m ) = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) )
82 eqeq12 
 |-  ( ( x = ( seq 1 ( x. , G ) ` m ) /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) -> ( x = z <-> ( seq 1 ( x. , G ) ` m ) = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) )
83 81 82 syl5ibrcom 
 |-  ( ( ( ph /\ ( m e. NN /\ w e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... w ) -1-1-onto-> A ) ) -> ( ( x = ( seq 1 ( x. , G ) ` m ) /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) -> x = z ) )
84 83 expimpd 
 |-  ( ( ph /\ ( m e. NN /\ w e. NN ) ) -> ( ( ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... w ) -1-1-onto-> A ) /\ ( x = ( seq 1 ( x. , G ) ` m ) /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) -> x = z ) )
85 69 84 biimtrid 
 |-  ( ( ph /\ ( m e. NN /\ w e. NN ) ) -> ( ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) -> x = z ) )
86 85 exlimdvv 
 |-  ( ( ph /\ ( m e. NN /\ w e. NN ) ) -> ( E. f E. g ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) -> x = z ) )
87 86 rexlimdvva 
 |-  ( ph -> ( E. m e. NN E. w e. NN E. f E. g ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ ( g : ( 1 ... w ) -1-1-onto-> A /\ z = ( seq 1 ( x. , ( j e. NN |-> [_ ( g ` j ) / k ]_ B ) ) ` w ) ) ) -> x = z ) )
88 68 87 biimtrrid 
 |-  ( ph -> ( ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) -> x = z ) )
89 88 com12 
 |-  ( ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) -> ( ph -> x = z ) )
90 36 42 45 89 ccase 
 |-  ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) ) -> ( ph -> x = z ) )
91 90 com12 
 |-  ( ph -> ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) ) -> x = z ) )
92 91 alrimivv 
 |-  ( ph -> A. x A. z ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) ) -> x = z ) )
93 breq2 
 |-  ( x = z -> ( seq m ( x. , F ) ~~> x <-> seq m ( x. , F ) ~~> z ) )
94 93 3anbi3d 
 |-  ( x = z -> ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) <-> ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) ) )
95 94 rexbidv 
 |-  ( x = z -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) <-> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) ) )
96 eqeq1 
 |-  ( x = z -> ( x = ( seq 1 ( x. , G ) ` m ) <-> z = ( seq 1 ( x. , G ) ` m ) ) )
97 96 anbi2d 
 |-  ( x = z -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) )
98 97 exbidv 
 |-  ( x = z -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) )
99 98 rexbidv 
 |-  ( x = z -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) )
100 95 99 orbi12d 
 |-  ( x = z -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) ) )
101 100 mo4 
 |-  ( E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) <-> A. x A. z ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> z ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) ) ) -> x = z ) )
102 92 101 sylibr 
 |-  ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , G ) ` m ) ) ) )