# 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}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
prodmo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
prodmo.3
Assertion prodmo ${⊢}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\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 prodmo.1 ${⊢}{F}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
2 prodmo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
3 prodmo.3
4 3simpb ${⊢}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\to \left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)$
5 4 reximi ${⊢}\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\to \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)$
6 3simpb ${⊢}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\to \left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{z}\right)$
7 6 reximi ${⊢}\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\to \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{z}\right)$
8 fveq2 ${⊢}{m}={w}\to {ℤ}_{\ge {m}}={ℤ}_{\ge {w}}$
9 8 sseq2d ${⊢}{m}={w}\to \left({A}\subseteq {ℤ}_{\ge {m}}↔{A}\subseteq {ℤ}_{\ge {w}}\right)$
10 seqeq1 ${⊢}{m}={w}\to seq{m}\left(×,{F}\right)=seq{w}\left(×,{F}\right)$
11 10 breq1d ${⊢}{m}={w}\to \left(seq{m}\left(×,{F}\right)⇝{z}↔seq{w}\left(×,{F}\right)⇝{z}\right)$
12 9 11 anbi12d ${⊢}{m}={w}\to \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{z}\right)↔\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)$
13 12 cbvrexvw ${⊢}\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{z}\right)↔\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)$
14 13 anbi2i ${⊢}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{z}\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 {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)$
15 reeanv ${⊢}\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\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 {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)$
16 14 15 bitr4i ${⊢}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\right)↔\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)$
17 simprlr ${⊢}\left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\to seq{m}\left(×,{F}\right)⇝{x}$
18 17 adantl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\to seq{m}\left(×,{F}\right)⇝{x}$
19 2 adantlr ${⊢}\left(\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\wedge {k}\in {A}\right)\to {B}\in ℂ$
20 simprll ${⊢}\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\to {m}\in ℤ$
21 simprlr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\to {w}\in ℤ$
22 simprll ${⊢}\left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\to {A}\subseteq {ℤ}_{\ge {m}}$
23 22 adantl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\to {A}\subseteq {ℤ}_{\ge {m}}$
24 simprrl ${⊢}\left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\to {A}\subseteq {ℤ}_{\ge {w}}$
25 24 adantl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\to {A}\subseteq {ℤ}_{\ge {w}}$
26 1 19 20 21 23 25 prodrb ${⊢}\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\to \left(seq{m}\left(×,{F}\right)⇝{x}↔seq{w}\left(×,{F}\right)⇝{x}\right)$
27 18 26 mpbid ${⊢}\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\to seq{w}\left(×,{F}\right)⇝{x}$
28 simprrr ${⊢}\left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\to seq{w}\left(×,{F}\right)⇝{z}$
29 28 adantl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\to seq{w}\left(×,{F}\right)⇝{z}$
30 climuni ${⊢}\left(seq{w}\left(×,{F}\right)⇝{x}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\to {x}={z}$
31 27 29 30 syl2anc ${⊢}\left({\phi }\wedge \left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\right)\to {x}={z}$
32 31 expcom ${⊢}\left(\left({m}\in ℤ\wedge {w}\in ℤ\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\right)\to \left({\phi }\to {x}={z}\right)$
33 32 ex ${⊢}\left({m}\in ℤ\wedge {w}\in ℤ\right)\to \left(\left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\to \left({\phi }\to {x}={z}\right)\right)$
34 33 rexlimivv ${⊢}\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{z}\right)\right)\to \left({\phi }\to {x}={z}\right)$
35 16 34 sylbi ${⊢}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\right)\to \left({\phi }\to {x}={z}\right)$
36 5 7 35 syl2an ${⊢}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\wedge \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\right)\to \left({\phi }\to {x}={z}\right)$
37 1 2 3 prodmolem2 ${⊢}\left({\phi }\wedge \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\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 {z}={x}\right)$
38 equcomi ${⊢}{z}={x}\to {x}={z}$
39 37 38 syl6 ${⊢}\left({\phi }\wedge \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\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}={z}\right)$
40 39 expimpd ${⊢}{\phi }\to \left(\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\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 {x}={z}\right)$
41 40 com12 ${⊢}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\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({\phi }\to {x}={z}\right)$
42 41 ancoms ${⊢}\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)\wedge \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\right)\to \left({\phi }\to {x}={z}\right)$
43 1 2 3 prodmolem2 ${⊢}\left({\phi }\wedge \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\to {x}={z}\right)$
44 43 expimpd ${⊢}{\phi }\to \left(\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)\to {x}={z}\right)$
45 44 com12 ${⊢}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{x}\right)\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)\to \left({\phi }\to {x}={z}\right)$
46 reeanv
47 exdistrv
48 47 2rexbii
49 oveq2 ${⊢}{m}={w}\to \left(1\dots {m}\right)=\left(1\dots {w}\right)$
50 49 f1oeq2d ${⊢}{m}={w}\to \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}↔{f}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}\right)$
51 fveq2 ${⊢}{m}={w}\to seq1\left(×,{G}\right)\left({m}\right)=seq1\left(×,{G}\right)\left({w}\right)$
52 51 eqeq2d ${⊢}{m}={w}\to \left({z}=seq1\left(×,{G}\right)\left({m}\right)↔{z}=seq1\left(×,{G}\right)\left({w}\right)\right)$
53 50 52 anbi12d ${⊢}{m}={w}\to \left(\left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {z}=seq1\left(×,{G}\right)\left({m}\right)\right)↔\left({f}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}\wedge {z}=seq1\left(×,{G}\right)\left({w}\right)\right)\right)$
54 53 exbidv ${⊢}{m}={w}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {z}=seq1\left(×,{G}\right)\left({m}\right)\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}\wedge {z}=seq1\left(×,{G}\right)\left({w}\right)\right)\right)$
55 f1oeq1 ${⊢}{f}={g}\to \left({f}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}↔{g}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}\right)$
56 fveq1 ${⊢}{f}={g}\to {f}\left({j}\right)={g}\left({j}\right)$
57 56 csbeq1d
58 57 mpteq2dv
59 3 58 syl5eq
60 59 seqeq3d
61 60 fveq1d
62 61 eqeq2d
63 55 62 anbi12d
64 63 cbvexvw
65 54 64 syl6bb
66 65 cbvrexvw
67 66 anbi2i
68 46 48 67 3bitr4i
69 an4
70 2 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge \left({m}\in ℕ\wedge {w}\in ℕ\right)\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {k}\in {A}\right)\to {B}\in ℂ$
71 fveq2 ${⊢}{j}={a}\to {f}\left({j}\right)={f}\left({a}\right)$
72 71 csbeq1d
73 72 cbvmptv
74 3 73 eqtri
75 fveq2 ${⊢}{j}={a}\to {g}\left({j}\right)={g}\left({a}\right)$
76 75 csbeq1d
77 76 cbvmptv
78 simplr ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge {w}\in ℕ\right)\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left({m}\in ℕ\wedge {w}\in ℕ\right)$
79 simprl ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge {w}\in ℕ\right)\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}$
80 simprr ${⊢}\left(\left({\phi }\wedge \left({m}\in ℕ\wedge {w}\in ℕ\right)\right)\wedge \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\wedge {g}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {g}:\left(1\dots {w}\right)\underset{1-1 onto}{⟶}{A}$
81 1 70 74 77 78 79 80 prodmolem3
82 eqeq12
83 81 82 syl5ibrcom
84 83 expimpd
85 69 84 syl5bi
86 85 exlimdvv
87 86 rexlimdvva
88 68 87 syl5bir ${⊢}{\phi }\to \left(\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)\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)\to {x}={z}\right)$
89 88 com12 ${⊢}\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)\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)\to \left({\phi }\to {x}={z}\right)$
90 36 42 45 89 ccase ${⊢}\left(\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\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 \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)\right)\to \left({\phi }\to {x}={z}\right)$
91 90 com12 ${⊢}{\phi }\to \left(\left(\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\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 \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)\right)\to {x}={z}\right)$
92 91 alrimivv ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\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 \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)\right)\to {x}={z}\right)$
93 breq2 ${⊢}{x}={z}\to \left(seq{m}\left(×,{F}\right)⇝{x}↔seq{m}\left(×,{F}\right)⇝{z}\right)$
94 93 3anbi3d ${⊢}{x}={z}\to \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{x}\right)↔\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\right)$
95 94 rexbidv ${⊢}{x}={z}\to \left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{x}\right)↔\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\right)\right)$
96 eqeq1 ${⊢}{x}={z}\to \left({x}=seq1\left(×,{G}\right)\left({m}\right)↔{z}=seq1\left(×,{G}\right)\left({m}\right)\right)$
97 96 anbi2d ${⊢}{x}={z}\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)$
98 97 exbidv ${⊢}{x}={z}\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)$
99 98 rexbidv ${⊢}{x}={z}\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)$
100 95 99 orbi12d ${⊢}{x}={z}\to \left(\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\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 \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)\right)$
101 100 mo4 ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\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 {z}\phantom{\rule{.4em}{0ex}}\left(\left(\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\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 \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\wedge seq{m}\left(×,{F}\right)⇝{z}\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\right)\right)\to {x}={z}\right)$
102 92 101 sylibr ${⊢}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)\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)$