This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
prodmo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
prodmo.3 ⊢ 𝐺 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
Assertion prodmo ( 𝜑 → ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) )

Proof

Step Hyp Ref Expression
1 prodmo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
2 prodmo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 prodmo.3 ⊢ 𝐺 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
4 3simpb ⊢ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) → ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) )
5 4 reximi ⊢ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) → ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) )
6 3simpb ⊢ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) → ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) )
7 6 reximi ⊢ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) → ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) )
8 fveq2 ⊢ ( 𝑚 = 𝑤 → ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ 𝑤 ) )
9 8 sseq2d ⊢ ( 𝑚 = 𝑤 → ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ↔ 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ) )
10 seqeq1 ⊢ ( 𝑚 = 𝑤 → seq 𝑚 ( · , 𝐹 ) = seq 𝑤 ( · , 𝐹 ) )
11 10 breq1d ⊢ ( 𝑚 = 𝑤 → ( seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ↔ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) )
12 9 11 anbi12d ⊢ ( 𝑚 = 𝑤 → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) )
13 12 cbvrexvw ⊢ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ↔ ∃ 𝑤 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) )
14 13 anbi2i ⊢ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑤 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) )
15 reeanv ⊢ ( ∃ 𝑚 ∈ ℤ ∃ 𝑤 ∈ ℤ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑤 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) )
16 14 15 bitr4i ⊢ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ) ↔ ∃ 𝑚 ∈ ℤ ∃ 𝑤 ∈ ℤ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) )
17 simprlr ⊢ ( ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) → seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 )
18 17 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) → seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 )
19 2 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
20 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) → 𝑚 ∈ ℤ )
21 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) → 𝑤 ∈ ℤ )
22 simprll ⊢ ( ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) )
23 22 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) )
24 simprrl ⊢ ( ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) )
26 1 19 20 21 23 25 prodrb ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) → ( seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ↔ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑥 ) )
27 18 26 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) → seq 𝑤 ( · , 𝐹 ) ⇝ 𝑥 )
28 simprrr ⊢ ( ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) → seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 )
29 28 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) → seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 )
30 climuni ⊢ ( ( seq 𝑤 ( · , 𝐹 ) ⇝ 𝑥 ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) → 𝑥 = 𝑧 )
31 27 29 30 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) ) → 𝑥 = 𝑧 )
32 31 expcom ⊢ ( ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
33 32 ex ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ ) → ( ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) → ( 𝜑 → 𝑥 = 𝑧 ) ) )
34 33 rexlimivv ⊢ ( ∃ 𝑚 ∈ ℤ ∃ 𝑤 ∈ ℤ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑤 ) ∧ seq 𝑤 ( · , 𝐹 ) ⇝ 𝑧 ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
35 16 34 sylbi ⊢ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
36 5 7 35 syl2an ⊢ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
37 1 2 3 prodmolem2 ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) → 𝑧 = 𝑥 ) )
38 equcomi ⊢ ( 𝑧 = 𝑥 → 𝑥 = 𝑧 )
39 37 38 syl6 ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑧 ) )
40 39 expimpd ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) → 𝑥 = 𝑧 ) )
41 40 com12 ⊢ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
42 41 ancoms ⊢ ( ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
43 1 2 3 prodmolem2 ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑧 ) )
44 43 expimpd ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) → 𝑥 = 𝑧 ) )
45 44 com12 ⊢ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
46 reeanv ⊢ ( ∃ 𝑚 ∈ ℕ ∃ 𝑤 ∈ ℕ ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) ↔ ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑤 ∈ ℕ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) )
47 exdistrv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) ↔ ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) )
48 47 2rexbii ⊢ ( ∃ 𝑚 ∈ ℕ ∃ 𝑤 ∈ ℕ ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑤 ∈ ℕ ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) )
49 oveq2 ⊢ ( 𝑚 = 𝑤 → ( 1 ... 𝑚 ) = ( 1 ... 𝑤 ) )
50 49 f1oeq2d ⊢ ( 𝑚 = 𝑤 → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ↔ 𝑓 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) )
51 fveq2 ⊢ ( 𝑚 = 𝑤 → ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑤 ) )
52 51 eqeq2d ⊢ ( 𝑚 = 𝑤 → ( 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ↔ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑤 ) ) )
53 50 52 anbi12d ⊢ ( 𝑚 = 𝑤 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑤 ) ) ) )
54 53 exbidv ⊢ ( 𝑚 = 𝑤 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑤 ) ) ) )
55 f1oeq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ↔ 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) )
56 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) )
57 56 csbeq1d ⊢ ( 𝑓 = 𝑔 → ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
58 57 mpteq2dv ⊢ ( 𝑓 = 𝑔 → ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) )
59 3 58 eqtrid ⊢ ( 𝑓 = 𝑔 → 𝐺 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) )
60 59 seqeq3d ⊢ ( 𝑓 = 𝑔 → seq 1 ( · , 𝐺 ) = seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) )
61 60 fveq1d ⊢ ( 𝑓 = 𝑔 → ( seq 1 ( · , 𝐺 ) ‘ 𝑤 ) = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) )
62 61 eqeq2d ⊢ ( 𝑓 = 𝑔 → ( 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑤 ) ↔ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) )
63 55 62 anbi12d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑤 ) ) ↔ ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) )
64 63 cbvexvw ⊢ ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑤 ) ) ↔ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) )
65 54 64 bitrdi ⊢ ( 𝑚 = 𝑤 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) )
66 65 cbvrexvw ⊢ ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑤 ∈ ℕ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) )
67 66 anbi2i ⊢ ( ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑤 ∈ ℕ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) )
68 46 48 67 3bitr4i ⊢ ( ∃ 𝑚 ∈ ℕ ∃ 𝑤 ∈ ℕ ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) ↔ ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) )
69 an4 ⊢ ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) ↔ ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) ∧ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) )
70 2 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
71 fveq2 ⊢ ( 𝑗 = 𝑎 → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 𝑎 ) )
72 71 csbeq1d ⊢ ( 𝑗 = 𝑎 → ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑎 ) / 𝑘 ⦌ 𝐵 )
73 72 cbvmptv ⊢ ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑎 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑎 ) / 𝑘 ⦌ 𝐵 )
74 3 73 eqtri ⊢ 𝐺 = ( 𝑎 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑎 ) / 𝑘 ⦌ 𝐵 )
75 fveq2 ⊢ ( 𝑗 = 𝑎 → ( 𝑔 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑎 ) )
76 75 csbeq1d ⊢ ( 𝑗 = 𝑎 → ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑔 ‘ 𝑎 ) / 𝑘 ⦌ 𝐵 )
77 76 cbvmptv ⊢ ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑎 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑎 ) / 𝑘 ⦌ 𝐵 )
78 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) ) → ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) )
79 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 )
80 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) ) → 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 )
81 1 70 74 77 78 79 80 prodmolem3 ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) ) → ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) )
82 eqeq12 ⊢ ( ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) → ( 𝑥 = 𝑧 ↔ ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) )
83 81 82 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) → 𝑥 = 𝑧 ) )
84 83 expimpd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ) ∧ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) → 𝑥 = 𝑧 ) )
85 69 84 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) → 𝑥 = 𝑧 ) )
86 85 exlimdvv ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) → 𝑥 = 𝑧 ) )
87 86 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑤 ∈ ℕ ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ( 𝑔 : ( 1 ... 𝑤 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑤 ) ) ) → 𝑥 = 𝑧 ) )
88 68 87 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) → 𝑥 = 𝑧 ) )
89 88 com12 ⊢ ( ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
90 36 42 45 89 ccase ⊢ ( ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
91 90 com12 ⊢ ( 𝜑 → ( ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ) → 𝑥 = 𝑧 ) )
92 91 alrimivv ⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑧 ( ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ) → 𝑥 = 𝑧 ) )
93 breq2 ⊢ ( 𝑥 = 𝑧 → ( seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ↔ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) )
94 93 3anbi3d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ) )
95 94 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ) )
96 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ↔ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) )
97 96 anbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) )
98 97 exbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) )
99 98 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) )
100 95 99 orbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ) )
101 100 mo4 ⊢ ( ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑧 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑧 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) ) → 𝑥 = 𝑧 ) )
102 92 101 sylibr ⊢ ( 𝜑 → ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑚 ) ) ) )