MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prodmo Structured version   Visualization version   GIF version

Theorem prodmo 15898
Description: A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017.)
Hypotheses
Ref Expression
prodmo.1 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
prodmo.2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
prodmo.3 𝐺 = (𝑗 ∈ ℕ ↦ (𝑓𝑗) / 𝑘𝐵)
Assertion
Ref Expression
prodmo (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))))
Distinct variable groups:   𝐴,𝑘,𝑛   𝑘,𝐹,𝑛   𝜑,𝑘,𝑛   𝐴,𝑓,𝑗,𝑚,𝑥   𝐵,𝑓,𝑗,𝑚   𝑓,𝐹,𝑗,𝑘,𝑚   𝜑,𝑓,𝑥   𝑥,𝐹   𝑗,𝐺,𝑥   𝑗,𝑘,𝑚,𝜑,𝑥   𝑥,𝑛,𝜑   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)   𝐵(𝑥,𝑦,𝑘,𝑛)   𝐹(𝑦)   𝐺(𝑦,𝑓,𝑘,𝑚,𝑛)

Proof of Theorem prodmo
Dummy variables 𝑎 𝑔 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3simpb 1147 . . . . . . 7 ((𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) → (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))
21reximi 3079 . . . . . 6 (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))
3 3simpb 1147 . . . . . . 7 ((𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) → (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))
43reximi 3079 . . . . . 6 (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))
5 fveq2 6891 . . . . . . . . . . . 12 (𝑚 = 𝑤 → (ℤ𝑚) = (ℤ𝑤))
65sseq2d 4010 . . . . . . . . . . 11 (𝑚 = 𝑤 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐴 ⊆ (ℤ𝑤)))
7 seqeq1 13987 . . . . . . . . . . . 12 (𝑚 = 𝑤 → seq𝑚( · , 𝐹) = seq𝑤( · , 𝐹))
87breq1d 5152 . . . . . . . . . . 11 (𝑚 = 𝑤 → (seq𝑚( · , 𝐹) ⇝ 𝑧 ↔ seq𝑤( · , 𝐹) ⇝ 𝑧))
96, 8anbi12d 630 . . . . . . . . . 10 (𝑚 = 𝑤 → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ↔ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
109cbvrexvw 3230 . . . . . . . . 9 (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ↔ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))
1110anbi2i 622 . . . . . . . 8 ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
12 reeanv 3221 . . . . . . . 8 (∃𝑚 ∈ ℤ ∃𝑤 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
1311, 12bitr4i 278 . . . . . . 7 ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ↔ ∃𝑚 ∈ ℤ ∃𝑤 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
14 simprlr 779 . . . . . . . . . . . . 13 (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → seq𝑚( · , 𝐹) ⇝ 𝑥)
1514adantl 481 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑚( · , 𝐹) ⇝ 𝑥)
16 prodmo.1 . . . . . . . . . . . . 13 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
17 prodmo.2 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
1817adantlr 714 . . . . . . . . . . . . 13 (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘𝐴) → 𝐵 ∈ ℂ)
19 simprll 778 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑚 ∈ ℤ)
20 simprlr 779 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑤 ∈ ℤ)
21 simprll 778 . . . . . . . . . . . . . 14 (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → 𝐴 ⊆ (ℤ𝑚))
2221adantl 481 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝐴 ⊆ (ℤ𝑚))
23 simprrl 780 . . . . . . . . . . . . . 14 (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → 𝐴 ⊆ (ℤ𝑤))
2423adantl 481 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝐴 ⊆ (ℤ𝑤))
2516, 18, 19, 20, 22, 24prodrb 15894 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → (seq𝑚( · , 𝐹) ⇝ 𝑥 ↔ seq𝑤( · , 𝐹) ⇝ 𝑥))
2615, 25mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑤( · , 𝐹) ⇝ 𝑥)
27 simprrr 781 . . . . . . . . . . . 12 (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → seq𝑤( · , 𝐹) ⇝ 𝑧)
2827adantl 481 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑤( · , 𝐹) ⇝ 𝑧)
29 climuni 15514 . . . . . . . . . . 11 ((seq𝑤( · , 𝐹) ⇝ 𝑥 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧) → 𝑥 = 𝑧)
3026, 28, 29syl2anc 583 . . . . . . . . . 10 ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑥 = 𝑧)
3130expcom 413 . . . . . . . . 9 (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → (𝜑𝑥 = 𝑧))
3231ex 412 . . . . . . . 8 ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) → (((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)) → (𝜑𝑥 = 𝑧)))
3332rexlimivv 3194 . . . . . . 7 (∃𝑚 ∈ ℤ ∃𝑤 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑤) ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)) → (𝜑𝑥 = 𝑧))
3413, 33sylbi 216 . . . . . 6 ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (𝜑𝑥 = 𝑧))
352, 4, 34syl2an 595 . . . . 5 ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (𝜑𝑥 = 𝑧))
36 prodmo.3 . . . . . . . . . 10 𝐺 = (𝑗 ∈ ℕ ↦ (𝑓𝑗) / 𝑘𝐵)
3716, 17, 36prodmolem2 15897 . . . . . . . . 9 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) → 𝑧 = 𝑥))
38 equcomi 2013 . . . . . . . . 9 (𝑧 = 𝑥𝑥 = 𝑧)
3937, 38syl6 35 . . . . . . . 8 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧))
4039expimpd 453 . . . . . . 7 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))) → 𝑥 = 𝑧))
4140com12 32 . . . . . 6 ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))) → (𝜑𝑥 = 𝑧))
4241ancoms 458 . . . . 5 ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (𝜑𝑥 = 𝑧))
4316, 17, 36prodmolem2 15897 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧))
4443expimpd 453 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚))) → 𝑥 = 𝑧))
4544com12 32 . . . . 5 ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚))) → (𝜑𝑥 = 𝑧))
46 reeanv 3221 . . . . . . . 8 (∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑤 ∈ ℕ ∃𝑔(𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))))
47 exdistrv 1952 . . . . . . . . 9 (∃𝑓𝑔((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))) ↔ (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))))
48472rexbii 3124 . . . . . . . 8 (∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ ∃𝑓𝑔((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))) ↔ ∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))))
49 oveq2 7422 . . . . . . . . . . . . . 14 (𝑚 = 𝑤 → (1...𝑚) = (1...𝑤))
5049f1oeq2d 6829 . . . . . . . . . . . . 13 (𝑚 = 𝑤 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑤)–1-1-onto𝐴))
51 fveq2 6891 . . . . . . . . . . . . . 14 (𝑚 = 𝑤 → (seq1( · , 𝐺)‘𝑚) = (seq1( · , 𝐺)‘𝑤))
5251eqeq2d 2738 . . . . . . . . . . . . 13 (𝑚 = 𝑤 → (𝑧 = (seq1( · , 𝐺)‘𝑚) ↔ 𝑧 = (seq1( · , 𝐺)‘𝑤)))
5350, 52anbi12d 630 . . . . . . . . . . . 12 (𝑚 = 𝑤 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑤))))
5453exbidv 1917 . . . . . . . . . . 11 (𝑚 = 𝑤 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑤))))
55 f1oeq1 6821 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓:(1...𝑤)–1-1-onto𝐴𝑔:(1...𝑤)–1-1-onto𝐴))
56 fveq1 6890 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑔 → (𝑓𝑗) = (𝑔𝑗))
5756csbeq1d 3893 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑔(𝑓𝑗) / 𝑘𝐵 = (𝑔𝑗) / 𝑘𝐵)
5857mpteq2dv 5244 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → (𝑗 ∈ ℕ ↦ (𝑓𝑗) / 𝑘𝐵) = (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))
5936, 58eqtrid 2779 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔𝐺 = (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))
6059seqeq3d 13992 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → seq1( · , 𝐺) = seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵)))
6160fveq1d 6893 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (seq1( · , 𝐺)‘𝑤) = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))
6261eqeq2d 2738 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑧 = (seq1( · , 𝐺)‘𝑤) ↔ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤)))
6355, 62anbi12d 630 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑤)) ↔ (𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))))
6463cbvexvw 2033 . . . . . . . . . . 11 (∃𝑓(𝑓:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑤)) ↔ ∃𝑔(𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤)))
6554, 64bitrdi 287 . . . . . . . . . 10 (𝑚 = 𝑤 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑔(𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))))
6665cbvrexvw 3230 . . . . . . . . 9 (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑤 ∈ ℕ ∃𝑔(𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤)))
6766anbi2i 622 . . . . . . . 8 ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑤 ∈ ℕ ∃𝑔(𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))))
6846, 48, 673bitr4i 303 . . . . . . 7 (∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ ∃𝑓𝑔((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚))))
69 an4 655 . . . . . . . . . 10 (((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))) ↔ ((𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑤)–1-1-onto𝐴) ∧ (𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))))
7017ad4ant14 751 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑤)–1-1-onto𝐴)) ∧ 𝑘𝐴) → 𝐵 ∈ ℂ)
71 fveq2 6891 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑎 → (𝑓𝑗) = (𝑓𝑎))
7271csbeq1d 3893 . . . . . . . . . . . . . . 15 (𝑗 = 𝑎(𝑓𝑗) / 𝑘𝐵 = (𝑓𝑎) / 𝑘𝐵)
7372cbvmptv 5255 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ ↦ (𝑓𝑗) / 𝑘𝐵) = (𝑎 ∈ ℕ ↦ (𝑓𝑎) / 𝑘𝐵)
7436, 73eqtri 2755 . . . . . . . . . . . . 13 𝐺 = (𝑎 ∈ ℕ ↦ (𝑓𝑎) / 𝑘𝐵)
75 fveq2 6891 . . . . . . . . . . . . . . 15 (𝑗 = 𝑎 → (𝑔𝑗) = (𝑔𝑎))
7675csbeq1d 3893 . . . . . . . . . . . . . 14 (𝑗 = 𝑎(𝑔𝑗) / 𝑘𝐵 = (𝑔𝑎) / 𝑘𝐵)
7776cbvmptv 5255 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵) = (𝑎 ∈ ℕ ↦ (𝑔𝑎) / 𝑘𝐵)
78 simplr 768 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑤)–1-1-onto𝐴)) → (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ))
79 simprl 770 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑤)–1-1-onto𝐴)) → 𝑓:(1...𝑚)–1-1-onto𝐴)
80 simprr 772 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑤)–1-1-onto𝐴)) → 𝑔:(1...𝑤)–1-1-onto𝐴)
8116, 70, 74, 77, 78, 79, 80prodmolem3 15895 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑤)–1-1-onto𝐴)) → (seq1( · , 𝐺)‘𝑚) = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))
82 eqeq12 2744 . . . . . . . . . . . 12 ((𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤)) → (𝑥 = 𝑧 ↔ (seq1( · , 𝐺)‘𝑚) = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤)))
8381, 82syl5ibrcom 246 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑤)–1-1-onto𝐴)) → ((𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤)) → 𝑥 = 𝑧))
8483expimpd 453 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑤)–1-1-onto𝐴) ∧ (𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))) → 𝑥 = 𝑧))
8569, 84biimtrid 241 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))) → 𝑥 = 𝑧))
8685exlimdvv 1930 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (∃𝑓𝑔((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))) → 𝑥 = 𝑧))
8786rexlimdvva 3206 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ ∃𝑓𝑔((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto𝐴𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ (𝑔𝑗) / 𝑘𝐵))‘𝑤))) → 𝑥 = 𝑧))
8868, 87biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚))) → 𝑥 = 𝑧))
8988com12 32 . . . . 5 ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚))) → (𝜑𝑥 = 𝑧))
9035, 42, 45, 89ccase 1036 . . . 4 (((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)))) → (𝜑𝑥 = 𝑧))
9190com12 32 . . 3 (𝜑 → (((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)))) → 𝑥 = 𝑧))
9291alrimivv 1924 . 2 (𝜑 → ∀𝑥𝑧(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)))) → 𝑥 = 𝑧))
93 breq2 5146 . . . . . 6 (𝑥 = 𝑧 → (seq𝑚( · , 𝐹) ⇝ 𝑥 ↔ seq𝑚( · , 𝐹) ⇝ 𝑧))
94933anbi3d 1439 . . . . 5 (𝑥 = 𝑧 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)))
9594rexbidv 3173 . . . 4 (𝑥 = 𝑧 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)))
96 eqeq1 2731 . . . . . . 7 (𝑥 = 𝑧 → (𝑥 = (seq1( · , 𝐺)‘𝑚) ↔ 𝑧 = (seq1( · , 𝐺)‘𝑚)))
9796anbi2d 628 . . . . . 6 (𝑥 = 𝑧 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚))))
9897exbidv 1917 . . . . 5 (𝑥 = 𝑧 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚))))
9998rexbidv 3173 . . . 4 (𝑥 = 𝑧 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚))))
10095, 99orbi12d 917 . . 3 (𝑥 = 𝑧 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)))))
101100mo4 2555 . 2 (∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))) ↔ ∀𝑥𝑧(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑧 = (seq1( · , 𝐺)‘𝑚)))) → 𝑥 = 𝑧))
10292, 101sylibr 233 1 (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , 𝐺)‘𝑚))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 846  w3a 1085  wal 1532   = wceq 1534  wex 1774  wcel 2099  ∃*wmo 2527  wne 2935  wrex 3065  csb 3889  wss 3944  ifcif 4524   class class class wbr 5142  cmpt 5225  1-1-ontowf1o 6541  cfv 6542  (class class class)co 7414  cc 11122  0cc0 11124  1c1 11125   · cmul 11129  cn 12228  cz 12574  cuz 12838  ...cfz 13502  seqcseq 13984  cli 15446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-inf2 9650  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201  ax-pre-sup 11202
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7863  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-er 8716  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-sup 9451  df-oi 9519  df-card 9948  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-sub 11462  df-neg 11463  df-div 11888  df-nn 12229  df-2 12291  df-3 12292  df-n0 12489  df-z 12575  df-uz 12839  df-rp 12993  df-fz 13503  df-fzo 13646  df-seq 13985  df-exp 14045  df-hash 14308  df-cj 15064  df-re 15065  df-im 15066  df-sqrt 15200  df-abs 15201  df-clim 15450
This theorem is referenced by:  fprod  15903
  Copyright terms: Public domain W3C validator