Metamath Proof Explorer

Theorem summo

Description: A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014) (Revised by Mario Carneiro, 23-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 summo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
2 summo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 summo.3 
 |-  G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
4 fveq2 
 |-  ( m = n -> ( ZZ>= ` m ) = ( ZZ>= ` n ) )
5 4 sseq2d 
 |-  ( m = n -> ( A C_ ( ZZ>= ` m ) <-> A C_ ( ZZ>= ` n ) ) )
6 seqeq1 
 |-  ( m = n -> seq m ( + , F ) = seq n ( + , F ) )
7 6 breq1d 
 |-  ( m = n -> ( seq m ( + , F ) ~~> y <-> seq n ( + , F ) ~~> y ) )
8 5 7 anbi12d 
 |-  ( m = n -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) <-> ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) )
9 8 cbvrexvw 
 |-  ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) <-> E. n e. ZZ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) )
10 reeanv 
 |-  ( E. m e. ZZ E. n e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ E. n e. ZZ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) )
11 simprlr 
 |-  ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> seq m ( + , F ) ~~> x )
12 2 ad4ant14 
 |-  ( ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) /\ k e. A ) -> B e. CC )
13 simplrl 
 |-  ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> m e. ZZ )
14 simplrr 
 |-  ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> n e. ZZ )
15 simprll 
 |-  ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> A C_ ( ZZ>= ` m ) )
16 simprrl 
 |-  ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> A C_ ( ZZ>= ` n ) )
17 1 12 13 14 15 16 sumrb 
 |-  ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> ( seq m ( + , F ) ~~> x <-> seq n ( + , F ) ~~> x ) )
18 11 17 mpbid 
 |-  ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> seq n ( + , F ) ~~> x )
19 simprrr 
 |-  ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> seq n ( + , F ) ~~> y )
20 climuni 
 |-  ( ( seq n ( + , F ) ~~> x /\ seq n ( + , F ) ~~> y ) -> x = y )
21 18 19 20 syl2anc 
 |-  ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> x = y )
22 21 exp31 
 |-  ( ph -> ( ( m e. ZZ /\ n e. ZZ ) -> ( ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) -> x = y ) ) )
23 22 rexlimdvv 
 |-  ( ph -> ( E. m e. ZZ E. n e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) -> x = y ) )
24 10 23 syl5bir 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ E. n e. ZZ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) -> x = y ) )
25 24 expdimp 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( E. n e. ZZ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) -> x = y ) )
26 9 25 syl5bi 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) -> x = y ) )
27 1 2 3 summolem2 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
28 26 27 jaod 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) -> x = y ) )
29 1 2 3 summolem2 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) -> y = x ) )
30 equcom 
 |-  ( y = x <-> x = y )
31 29 30 syl6ib 
 |-  ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
32 31 impancom 
 |-  ( ( ph /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) -> x = y ) )
33 oveq2 
 |-  ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
34 33 f1oeq2d 
 |-  ( m = n -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... n ) -1-1-onto-> A ) )
35 fveq2 
 |-  ( m = n -> ( seq 1 ( + , G ) ` m ) = ( seq 1 ( + , G ) ` n ) )
36 35 eqeq2d 
 |-  ( m = n -> ( y = ( seq 1 ( + , G ) ` m ) <-> y = ( seq 1 ( + , G ) ` n ) ) )
37 34 36 anbi12d 
 |-  ( m = n -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) <-> ( f : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` n ) ) ) )
38 37 exbidv 
 |-  ( m = n -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) <-> E. f ( f : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` n ) ) ) )
39 f1oeq1 
 |-  ( f = g -> ( f : ( 1 ... n ) -1-1-onto-> A <-> g : ( 1 ... n ) -1-1-onto-> A ) )
40 fveq1 
 |-  ( f = g -> ( f ` n ) = ( g ` n ) )
41 40 csbeq1d 
 |-  ( f = g -> [_ ( f ` n ) / k ]_ B = [_ ( g ` n ) / k ]_ B )
42 41 mpteq2dv 
 |-  ( f = g -> ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) )
43 3 42 syl5eq 
 |-  ( f = g -> G = ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) )
44 43 seqeq3d 
 |-  ( f = g -> seq 1 ( + , G ) = seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) )
45 44 fveq1d 
 |-  ( f = g -> ( seq 1 ( + , G ) ` n ) = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) )
46 45 eqeq2d 
 |-  ( f = g -> ( y = ( seq 1 ( + , G ) ` n ) <-> y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) )
47 39 46 anbi12d 
 |-  ( f = g -> ( ( f : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` n ) ) <-> ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
48 47 cbvexvw 
 |-  ( E. f ( f : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` n ) ) <-> E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) )
49 38 48 syl6bb 
 |-  ( m = n -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) <-> E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
50 49 cbvrexvw 
 |-  ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) <-> E. n e. NN E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) )
51 reeanv 
 |-  ( E. m e. NN E. n e. NN ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) <-> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. n e. NN E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
52 exdistrv 
 |-  ( E. f E. g ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) <-> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
53 an4 
 |-  ( ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) <-> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) /\ ( x = ( seq 1 ( + , G ) ` m ) /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
54 2 ad4ant14 
 |-  ( ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) /\ k e. A ) -> B e. CC )
55 fveq2 
 |-  ( n = j -> ( f ` n ) = ( f ` j ) )
56 55 csbeq1d 
 |-  ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / k ]_ B )
57 56 cbvmptv 
 |-  ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
58 3 57 eqtri 
 |-  G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
59 fveq2 
 |-  ( n = j -> ( g ` n ) = ( g ` j ) )
60 59 csbeq1d 
 |-  ( n = j -> [_ ( g ` n ) / k ]_ B = [_ ( g ` j ) / k ]_ B )
61 60 cbvmptv 
 |-  ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) = ( j e. NN |-> [_ ( g ` j ) / k ]_ B )
62 simplr 
 |-  ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> ( m e. NN /\ n e. NN ) )
63 simprl 
 |-  ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> f : ( 1 ... m ) -1-1-onto-> A )
64 simprr 
 |-  ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> g : ( 1 ... n ) -1-1-onto-> A )
65 1 54 58 61 62 63 64 summolem3 
 |-  ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> ( seq 1 ( + , G ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) )
66 eqeq12 
 |-  ( ( x = ( seq 1 ( + , G ) ` m ) /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) -> ( x = y <-> ( seq 1 ( + , G ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) )
67 65 66 syl5ibrcom 
 |-  ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> ( ( x = ( seq 1 ( + , G ) ` m ) /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) -> x = y ) )
68 67 expimpd 
 |-  ( ( ph /\ ( m e. NN /\ n e. NN ) ) -> ( ( ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) /\ ( x = ( seq 1 ( + , G ) ` m ) /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
69 53 68 syl5bi 
 |-  ( ( ph /\ ( m e. NN /\ n e. NN ) ) -> ( ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
70 69 exlimdvv 
 |-  ( ( ph /\ ( m e. NN /\ n e. NN ) ) -> ( E. f E. g ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
71 52 70 syl5bir 
 |-  ( ( ph /\ ( m e. NN /\ n e. NN ) ) -> ( ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
72 71 rexlimdvva 
 |-  ( ph -> ( E. m e. NN E. n e. NN ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
73 51 72 syl5bir 
 |-  ( ph -> ( ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. n e. NN E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
74 73 expdimp 
 |-  ( ( ph /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) -> ( E. n e. NN E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) -> x = y ) )
75 50 74 syl5bi 
 |-  ( ( ph /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
76 32 75 jaod 
 |-  ( ( ph /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) -> x = y ) )
77 28 76 jaodan 
 |-  ( ( ph /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) -> x = y ) )
78 77 expimpd 
 |-  ( ph -> ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) ) -> x = y ) )
79 78 alrimivv 
 |-  ( ph -> A. x A. y ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) ) -> x = y ) )
80 breq2 
 |-  ( x = y -> ( seq m ( + , F ) ~~> x <-> seq m ( + , F ) ~~> y ) )
81 80 anbi2d 
 |-  ( x = y -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) <-> ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) ) )
82 81 rexbidv 
 |-  ( x = y -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) <-> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) ) )
83 eqeq1 
 |-  ( x = y -> ( x = ( seq 1 ( + , G ) ` m ) <-> y = ( seq 1 ( + , G ) ` m ) ) )
84 83 anbi2d 
 |-  ( x = y -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) )
85 84 exbidv 
 |-  ( x = y -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) )
86 85 rexbidv 
 |-  ( x = y -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) )
87 82 86 orbi12d 
 |-  ( x = y -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) ) )
88 87 mo4 
 |-  ( E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) <-> A. x A. y ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) ) -> x = y ) )
89 79 88 sylibr 
 |-  ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) )