# Metamath Proof Explorer

## Theorem prodmolem2

Description: Lemma for prodmo . (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 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)$

### 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 fveq2 ${⊢}{m}={w}\to {ℤ}_{\ge {m}}={ℤ}_{\ge {w}}$
7 6 sseq2d ${⊢}{m}={w}\to \left({A}\subseteq {ℤ}_{\ge {m}}↔{A}\subseteq {ℤ}_{\ge {w}}\right)$
8 seqeq1 ${⊢}{m}={w}\to seq{m}\left(×,{F}\right)=seq{w}\left(×,{F}\right)$
9 8 breq1d ${⊢}{m}={w}\to \left(seq{m}\left(×,{F}\right)⇝{x}↔seq{w}\left(×,{F}\right)⇝{x}\right)$
10 7 9 anbi12d ${⊢}{m}={w}\to \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)↔\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\right)$
11 10 cbvrexvw ${⊢}\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge seq{m}\left(×,{F}\right)⇝{x}\right)↔\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)$
12 reeanv ${⊢}\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge \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)↔\left(\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\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)$
13 simprlr ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to seq{w}\left(×,{F}\right)⇝{x}$
14 simprll ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {A}\subseteq {ℤ}_{\ge {w}}$
15 uzssz ${⊢}{ℤ}_{\ge {w}}\subseteq ℤ$
16 zssre ${⊢}ℤ\subseteq ℝ$
17 15 16 sstri ${⊢}{ℤ}_{\ge {w}}\subseteq ℝ$
18 14 17 sstrdi ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {A}\subseteq ℝ$
19 ltso ${⊢}<\mathrm{Or}ℝ$
20 soss ${⊢}{A}\subseteq ℝ\to \left(<\mathrm{Or}ℝ\to <\mathrm{Or}{A}\right)$
21 18 19 20 mpisyl ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to <\mathrm{Or}{A}$
22 fzfi ${⊢}\left(1\dots {m}\right)\in \mathrm{Fin}$
23 ovex ${⊢}\left(1\dots {m}\right)\in \mathrm{V}$
24 23 f1oen ${⊢}{f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\to \left(1\dots {m}\right)\approx {A}$
25 24 ad2antll ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left(1\dots {m}\right)\approx {A}$
26 25 ensymd ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {A}\approx \left(1\dots {m}\right)$
27 enfii ${⊢}\left(\left(1\dots {m}\right)\in \mathrm{Fin}\wedge {A}\approx \left(1\dots {m}\right)\right)\to {A}\in \mathrm{Fin}$
28 22 26 27 sylancr ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {A}\in \mathrm{Fin}$
29 fz1iso ${⊢}\left(<\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}{g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)$
30 21 28 29 syl2anc ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}{g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)$
31 2 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\wedge {k}\in {A}\right)\to {B}\in ℂ$
32 eqid
33 simplrr ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {m}\in ℕ$
34 simplrl ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {w}\in ℤ$
35 simplll ${⊢}\left(\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\to {A}\subseteq {ℤ}_{\ge {w}}$
36 35 adantl ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {A}\subseteq {ℤ}_{\ge {w}}$
37 simprlr ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}$
38 simprr ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)$
39 1 31 3 32 33 34 36 37 38 prodmolem2a ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\right)\right)\to seq{w}\left(×,{F}\right)⇝seq1\left(×,{G}\right)\left({m}\right)$
40 39 expr ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left({g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\to seq{w}\left(×,{F}\right)⇝seq1\left(×,{G}\right)\left({m}\right)\right)$
41 40 exlimdv ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left(\exists {g}\phantom{\rule{.4em}{0ex}}{g}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\to seq{w}\left(×,{F}\right)⇝seq1\left(×,{G}\right)\left({m}\right)\right)$
42 30 41 mpd ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to seq{w}\left(×,{F}\right)⇝seq1\left(×,{G}\right)\left({m}\right)$
43 climuni ${⊢}\left(seq{w}\left(×,{F}\right)⇝{x}\wedge seq{w}\left(×,{F}\right)⇝seq1\left(×,{G}\right)\left({m}\right)\right)\to {x}=seq1\left(×,{G}\right)\left({m}\right)$
44 13 42 43 syl2anc ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {x}=seq1\left(×,{G}\right)\left({m}\right)$
45 eqeq2 ${⊢}{z}=seq1\left(×,{G}\right)\left({m}\right)\to \left({x}={z}↔{x}=seq1\left(×,{G}\right)\left({m}\right)\right)$
46 44 45 syl5ibrcom ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left({z}=seq1\left(×,{G}\right)\left({m}\right)\to {x}={z}\right)$
47 46 expr ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\right)\to \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\to \left({z}=seq1\left(×,{G}\right)\left({m}\right)\to {x}={z}\right)\right)$
48 47 impd ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\right)\to \left(\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)$
49 48 exlimdv ${⊢}\left(\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\wedge \left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\right)\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)\to {x}={z}\right)$
50 49 expimpd ${⊢}\left({\phi }\wedge \left({w}\in ℤ\wedge {m}\in ℕ\right)\right)\to \left(\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge \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)$
51 50 rexlimdvva ${⊢}{\phi }\to \left(\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\left(×,{F}\right)⇝{x}\right)\wedge \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)$
52 12 51 syl5bir ${⊢}{\phi }\to \left(\left(\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\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)$
53 52 expdimp ${⊢}\left({\phi }\wedge \exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {w}}\wedge seq{w}\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)$
54 11 53 sylan2b ${⊢}\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 {z}=seq1\left(×,{G}\right)\left({m}\right)\right)\to {x}={z}\right)$
55 5 54 sylan2 ${⊢}\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)$