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 ( · , 𝐺 ) ‘ 𝑚 ) ) ) )