# 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}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)$
summo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
summo.3
Assertion summo ${⊢}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(+,{F}\right)⇝{x}\right)\vee \exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {x}=seq1\left(+,{G}\right)\left({m}\right)\right)\right)$

### Proof

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