Metamath Proof Explorer

Theorem summo

Description: A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
summo.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
Assertion summo ( 𝜑 → ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) )

Proof

Step Hyp Ref Expression
1 summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
2 summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 summo.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
4 fveq2 ⊢ ( 𝑚 = 𝑛 → ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ 𝑛 ) )
5 4 sseq2d ⊢ ( 𝑚 = 𝑛 → ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ↔ 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ) )
6 seqeq1 ⊢ ( 𝑚 = 𝑛 → seq 𝑚 ( + , 𝐹 ) = seq 𝑛 ( + , 𝐹 ) )
7 6 breq1d ⊢ ( 𝑚 = 𝑛 → ( seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ↔ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) )
8 5 7 anbi12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) )
9 8 cbvrexvw ⊢ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) )
10 reeanv ⊢ ( ∃ 𝑚 ∈ ℤ ∃ 𝑛 ∈ ℤ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑛 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) )
11 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) → seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 )
12 2 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
13 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) → 𝑚 ∈ ℤ )
14 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) → 𝑛 ∈ ℤ )
15 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) )
16 simprrl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) )
17 1 12 13 14 15 16 sumrb ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) → ( seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ↔ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑥 ) )
18 11 17 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) → seq 𝑛 ( + , 𝐹 ) ⇝ 𝑥 )
19 simprrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) → seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 )
20 climuni ⊢ ( ( seq 𝑛 ( + , 𝐹 ) ⇝ 𝑥 ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) → 𝑥 = 𝑦 )
21 18 19 20 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) ∧ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) ) → 𝑥 = 𝑦 )
22 21 exp31 ⊢ ( 𝜑 → ( ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) → 𝑥 = 𝑦 ) ) )
23 22 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℤ ∃ 𝑛 ∈ ℤ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) → 𝑥 = 𝑦 ) )
24 10 23 syl5bir ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∧ ∃ 𝑛 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) ) → 𝑥 = 𝑦 ) )
25 24 expdimp ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ) → ( ∃ 𝑛 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑛 ) ∧ seq 𝑛 ( + , 𝐹 ) ⇝ 𝑦 ) → 𝑥 = 𝑦 ) )
26 9 25 syl5bi ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) → 𝑥 = 𝑦 ) )
27 1 2 3 summolem2 ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑦 ) )
28 26 27 jaod ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) → 𝑥 = 𝑦 ) )
29 1 2 3 summolem2 ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑦 = 𝑥 ) )
30 equcom ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
31 29 30 syl6ib ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑦 ) )
32 31 impancom ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) → 𝑥 = 𝑦 ) )
33 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 1 ... 𝑚 ) = ( 1 ... 𝑛 ) )
34 33 f1oeq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ↔ 𝑓 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ) )
35 fveq2 ⊢ ( 𝑚 = 𝑛 → ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) )
36 35 eqeq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ↔ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) ) )
37 34 36 anbi12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) ) ) )
38 37 exbidv ⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) ) ) )
39 f1oeq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ↔ 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ) )
40 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑛 ) )
41 40 csbeq1d ⊢ ( 𝑓 = 𝑔 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
42 41 mpteq2dv ⊢ ( 𝑓 = 𝑔 → ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) )
43 3 42 syl5eq ⊢ ( 𝑓 = 𝑔 → 𝐺 = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) )
44 43 seqeq3d ⊢ ( 𝑓 = 𝑔 → seq 1 ( + , 𝐺 ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) )
45 44 fveq1d ⊢ ( 𝑓 = 𝑔 → ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) )
46 45 eqeq2d ⊢ ( 𝑓 = 𝑔 → ( 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) ↔ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) )
47 39 46 anbi12d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) ) ↔ ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) )
48 47 cbvexvw ⊢ ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) ) ↔ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) )
49 38 48 syl6bb ⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) )
50 49 cbvrexvw ⊢ ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) )
51 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 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) )
52 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 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) )
53 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 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) )
54 2 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
55 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑗 ) )
56 55 csbeq1d ⊢ ( 𝑛 = 𝑗 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
57 56 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
58 3 57 eqtri ⊢ 𝐺 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
59 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑗 ) )
60 59 csbeq1d ⊢ ( 𝑛 = 𝑗 → ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
61 60 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
62 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ) ) → ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) )
63 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 )
64 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ) ) → 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 )
65 1 54 58 61 62 63 64 summolem3 ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ) ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) )
66 eqeq12 ⊢ ( ( 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) → ( 𝑥 = 𝑦 ↔ ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) )
67 65 66 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑥 = 𝑦 ) )
68 67 expimpd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ) ∧ ( 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) → 𝑥 = 𝑦 ) )
69 53 68 syl5bi ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) → 𝑥 = 𝑦 ) )
70 69 exlimdvv ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) → 𝑥 = 𝑦 ) )
71 52 70 syl5bir ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) → 𝑥 = 𝑦 ) )
72 71 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) → 𝑥 = 𝑦 ) )
73 51 72 syl5bir ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ∧ ∃ 𝑛 ∈ ℕ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) ) → 𝑥 = 𝑦 ) )
74 73 expdimp ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑥 = 𝑦 ) )
75 50 74 syl5bi ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) → 𝑥 = 𝑦 ) )
76 32 75 jaod ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) → 𝑥 = 𝑦 ) )
77 28 76 jaodan ⊢ ( ( 𝜑 ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) → 𝑥 = 𝑦 ) )
78 77 expimpd ⊢ ( 𝜑 → ( ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ) → 𝑥 = 𝑦 ) )
79 78 alrimivv ⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ) → 𝑥 = 𝑦 ) )
80 breq2 ⊢ ( 𝑥 = 𝑦 → ( seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ↔ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) )
81 80 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ) )
82 81 rexbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ) )
83 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ↔ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) )
84 83 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) )
85 84 exbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) )
86 85 rexbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) )
87 82 86 orbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ) )
88 87 mo4 ⊢ ( ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) ) → 𝑥 = 𝑦 ) )
89 79 88 sylibr ⊢ ( 𝜑 → ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , 𝐹 ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , 𝐺 ) ‘ 𝑚 ) ) ) )