summodc - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > summodc		GIF version

Theorem summodc 12133

Description: A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.)

**Hypotheses**
Ref	Expression
isummo.1	⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
isummo.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
summodclem2.g	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
summodc.3	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))

**Assertion**
Ref	Expression
summodc	⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))))

Distinct variable groups: 𝑘,𝑛,𝐴 𝑛,𝐹 𝜑,𝑘,𝑛 𝐴,𝑓,𝑗,𝑚,𝑘,𝑛 𝐵,𝑛 𝑓,𝐹,𝑘,𝑚 𝜑,𝑓,𝑚,𝑥,𝑘,𝑛 𝑥,𝐴,𝑗 𝐵,𝑓,𝑗,𝑚 𝑗,𝐹,𝑥 𝑛,𝐺,𝑥 𝜑,𝑗,𝑥 Allowed substitution hints: 𝐵(𝑥,𝑘) 𝐺(𝑓,𝑗,𝑘,𝑚)

Proof of Theorem summodc Dummy variables 𝑎 𝑔 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5693	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑛))
2	1	sseq2d 3278	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ (ℤ_≥‘𝑛)))
3	1	raleqdv 2755	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴))
4		seqeq1 10870	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → seq𝑚( + , 𝐹) = seq𝑛( + , 𝐹))
5	4	breq1d 4138	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (seq𝑚( + , 𝐹) ⇝ 𝑦 ↔ seq𝑛( + , 𝐹) ⇝ 𝑦))
6	2, 3, 5	3anbi123d 1353	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
7	6	cbvrexv 2787	. . . . . . 7 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))
8		reeanv 2721	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
9		simprl3 1075	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑚( + , 𝐹) ⇝ 𝑥)
10		isummo.1	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
11		simpll 531	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝜑)
12		isummo.2	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
13	11, 12	sylan 283	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
14		simplrl 541	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑚 ∈ ℤ)
15		simplrr 542	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑛 ∈ ℤ)
16		simprl1 1073	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ_≥‘𝑚))
17		simprr1 1076	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ_≥‘𝑛))
18		eleq1w 2299	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
19	18	dcbid 850	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴))
20		simprl2 1074	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
21	20	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
22		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → 𝑘 ∈ (ℤ_≥‘𝑚))
23	19, 21, 22	rspcdva 2934	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → DECID 𝑘 ∈ 𝐴)
24		simprr2 1077	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴)
25	24	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴)
26		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → 𝑘 ∈ (ℤ_≥‘𝑛))
27	19, 25, 26	rspcdva 2934	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → DECID 𝑘 ∈ 𝐴)
28	10, 13, 14, 15, 16, 17, 23, 27	sumrbdc 12129	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑛( + , 𝐹) ⇝ 𝑥))
29	9, 28	mpbid 147	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑥)
30		simprr3 1078	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑦)
31		climuni 12042	. . . . . . . . . . . 12 ⊢ ((seq𝑛( + , 𝐹) ⇝ 𝑥 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦)
32	29, 30, 31	syl2anc 415	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑥 = 𝑦)
33	32	exp31 364	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦)))
34	33	rexlimdvv 2675	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
35	8, 34	biimtrrid 153	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
36	35	expdimp 259	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
37	7, 36	biimtrid 152	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
38		summodc.3	. . . . . . 7 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
39	10, 12, 38	summodclem2 12132	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
40	37, 39	jaod 729	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
41	10, 12, 38	summodclem2 12132	. . . . . . . 8 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑦 = 𝑥))
42		equcom 1758	. . . . . . . 8 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
43	41, 42	imbitrdi 161	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
44	43	impancom 260	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
45		oveq2 6087	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
46		f1oeq2 5626	. . . . . . . . . . . 12 ⊢ ((1...𝑚) = (1...𝑛) → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑛)–1-1-onto→𝐴))
47	45, 46	syl 14	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑛)–1-1-onto→𝐴))
48		fveq2 5693	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘𝑛))
49	48	eqeq2d 2250	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑦 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑛)))
50	47, 49	anbi12d 477	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛))))
51	50	exbidv 1878	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛))))
52		f1oeq1 5625	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑓:(1...𝑛)–1-1-onto→𝐴 ↔ 𝑔:(1...𝑛)–1-1-onto→𝐴))
53		breq1 4131	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑎 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑎 ≤ (♯‘𝐴)))
54		fveq2 5693	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑎 → (𝑓‘𝑛) = (𝑓‘𝑎))
55	54	csbeq1d 3154	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑎 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑎) / 𝑘⦌𝐵)
56	53, 55	ifbieq1d 3663	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑎 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 0))
57	56	cbvmptv 4225	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 0))
58		fveq1 5692	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑎) = (𝑔‘𝑎))
59	58	csbeq1d 3154	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → ⦋(𝑓‘𝑎) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑎) / 𝑘⦌𝐵)
60	59	ifeq1d 3658	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 0) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))
61	60	mpteq2dv 4220	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))
62	57, 61	eqtrid 2283	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))
63	38, 62	eqtrid 2283	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → 𝐺 = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))
64	63	seqeq3d 10875	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → seq1( + , 𝐺) = seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))))
65	64	fveq1d 5695	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (seq1( + , 𝐺)‘𝑛) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))
66	65	eqeq2d 2250	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑦 = (seq1( + , 𝐺)‘𝑛) ↔ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)))
67	52, 66	anbi12d 477	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))))
68	67	cbvexv 1974	. . . . . . . . 9 ⊢ (∃𝑓(𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)))
69	51, 68	bitrdi 196	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))))
70	69	cbvrexv 2787	. . . . . . 7 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)))
71		reeanv 2721	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))))
72		eeanv 1992	. . . . . . . . . . 11 ⊢ (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))) ↔ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))))
73		an4 592	. . . . . . . . . . . . 13 ⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))) ↔ ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))))
74		1zzd 9654	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 1 ∈ ℤ)
75		simplrr 542	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑛 ∈ ℕ)
76	75	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑛 ∈ ℤ)
77	74, 76	fzfigd 10851	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (1...𝑛) ∈ Fin)
78		simprr 537	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑔:(1...𝑛)–1-1-onto→𝐴)
79	77, 78	fihasheqf1od 11211	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘(1...𝑛)) = (♯‘𝐴))
80	75	nnnn0d 9603	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑛 ∈ ℕ₀)
81		hashfz1 11205	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ℕ₀ → (♯‘(1...𝑛)) = 𝑛)
82	80, 81	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘(1...𝑛)) = 𝑛)
83	79, 82	eqtr3d 2273	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘𝐴) = 𝑛)
84	83	breq2d 4140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (𝑎 ≤ (♯‘𝐴) ↔ 𝑎 ≤ 𝑛))
85	84	ifbid 3662	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0) = if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))
86	85	mpteq2dv 4220	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))
87	86	seqeq3d 10875	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))))
88	87	fveq1d 5695	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))
89	88	eqeq2d 2250	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛) ↔ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)))
90	89	anbi2d 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)) ↔ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))))
91		simplrl 541	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑚 ∈ ℕ)
92	91	nnnn0d 9603	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑚 ∈ ℕ₀)
93		hashfz1 11205	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
94	92, 93	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘(1...𝑚)) = 𝑚)
95	91	nnzd 9750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑚 ∈ ℤ)
96	74, 95	fzfigd 10851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (1...𝑚) ∈ Fin)
97		simprl 535	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
98	96, 97	fihasheqf1od 11211	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘(1...𝑚)) = (♯‘𝐴))
99	94, 98	eqtr3d 2273	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑚 = (♯‘𝐴))
100	99	fveq2d 5697	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘(♯‘𝐴)))
101		simpll 531	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝜑)
102	101, 12	sylan 283	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
103	99, 91	eqeltrrd 2316	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘𝐴) ∈ ℕ)
104	103, 75	jca 306	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → ((♯‘𝐴) ∈ ℕ ∧ 𝑛 ∈ ℕ))
105	99	oveq2d 6095	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (1...𝑚) = (1...(♯‘𝐴)))
106		f1oeq2 5626	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...𝑚) = (1...(♯‘𝐴)) → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))
107	105, 106	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))
108	97, 107	mpbid 147	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)
109		breq1 4131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
110		fveq2 5693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
111	110	csbeq1d 3154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
112	109, 111	ifbieq1d 3663	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 0))
113	112	cbvmptv 4225	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 0))
114	38, 113	eqtri 2259	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 0))
115		breq1 4131	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑗 → (𝑎 ≤ 𝑛 ↔ 𝑗 ≤ 𝑛))
116		fveq2 5693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑗 → (𝑔‘𝑎) = (𝑔‘𝑗))
117	116	csbeq1d 3154	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑗 → ⦋(𝑔‘𝑎) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑗) / 𝑘⦌𝐵)
118	115, 117	ifbieq1d 3663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑗 → if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0) = if(𝑗 ≤ 𝑛, ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 0))
119	118	cbvmptv 4225	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ 𝑛, ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 0))
120	10, 102, 104, 108, 78, 114, 119	summodclem3 12130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))
121	100, 120	eqtrd 2271	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))
122		eqeq12 2251	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)) → (𝑥 = 𝑦 ↔ (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)))
123	121, 122	syl5ibrcom 157	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)) → 𝑥 = 𝑦))
124	90, 123	sylbid 150	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)) → 𝑥 = 𝑦))
125	124	expimpd 363	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
126	73, 125	biimtrid 152	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
127	126	exlimdvv 1953	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
128	72, 127	biimtrrid 153	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
129	128	rexlimdvva 2676	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
130	71, 129	biimtrrid 153	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))) → 𝑥 = 𝑦))
131	130	expdimp 259	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)) → 𝑥 = 𝑦))
132	70, 131	biimtrid 152	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
133	44, 132	jaod 729	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
134	40, 133	jaodan 809	. . . 4 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
135	134	expimpd 363	. . 3 ⊢ (𝜑 → (((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
136	135	alrimivv 1928	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
137		breq2 4132	. . . . . 6 ⊢ (𝑥 = 𝑦 → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑚( + , 𝐹) ⇝ 𝑦))
138	137	3anbi3d 1359	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
139	138	rexbidv 2551	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
140		eqeq1 2245	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑚)))
141	140	anbi2d 468	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
142	141	exbidv 1878	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
143	142	rexbidv 2551	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
144	139, 143	orbi12d 805	. . 3 ⊢ (𝑥 = 𝑦 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))))
145	144	mo4 2148	. 2 ⊢ (∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ ∀𝑥∀𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
146	136, 145	sylibr 134	1 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 ∧ w3a 1009 ∀wal 1400 = wceq 1402 ∃wex 1545 ∃*wmo 2087 ∈ wcel 2209 ∀wral 2528 ∃wrex 2529 ⦋csb 3147 ⊆ wss 3220 ifcif 3638 class class class wbr 4128 ↦ cmpt 4190 –1-1-onto→wf1o 5374 ‘cfv 5375 (class class class)co 6079 ℂcc 8171 0cc0 8173 1c1 8174 + caddc 8176 ≤ cle 8355 ℕcn 9287 ℕ₀cn0 9546 ℤcz 9627 ℤ_≥cuz 9904 ...cfz 10394 seqcseq 10867 ♯chash 11197 ⇝ cli 12027

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4244 ax-sep 4247 ax-nul 4257 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-iinf 4733 ax-cnex 8264 ax-resscn 8265 ax-1cn 8266 ax-1re 8267 ax-icn 8268 ax-addcl 8269 ax-addrcl 8270 ax-mulcl 8271 ax-mulrcl 8272 ax-addcom 8273 ax-mulcom 8274 ax-addass 8275 ax-mulass 8276 ax-distr 8277 ax-i2m1 8278 ax-0lt1 8279 ax-1rid 8280 ax-0id 8281 ax-rnegex 8282 ax-precex 8283 ax-cnre 8284 ax-pre-ltirr 8285 ax-pre-ltwlin 8286 ax-pre-lttrn 8287 ax-pre-apti 8288 ax-pre-ltadd 8289 ax-pre-mulgt0 8290 ax-pre-mulext 8291 ax-arch 8292 ax-caucvg 8293

This theorem depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-iun 4012 df-br 4129 df-opab 4191 df-mpt 4192 df-tr 4228 df-id 4436 df-po 4439 df-iso 4440 df-iord 4509 df-on 4511 df-ilim 4512 df-suc 4514 df-iom 4736 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-ima 4785 df-iota 5335 df-fun 5377 df-fn 5378 df-f 5379 df-f1 5380 df-fo 5381 df-f1o 5382 df-fv 5383 df-isom 5384 df-riota 6032 df-ov 6082 df-oprab 6083 df-mpo 6084 df-1st 6368 df-2nd 6369 df-recs 6570 df-irdg 6635 df-frec 6656 df-1o 6681 df-oadd 6685 df-er 6801 df-en 7017 df-dom 7018 df-fin 7019 df-pnf 8356 df-mnf 8357 df-xr 8358 df-ltxr 8359 df-le 8360 df-sub 8493 df-neg 8494 df-reap 8897 df-ap 8904 df-div 8997 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-n0 9547 df-z 9628 df-uz 9905 df-q 10003 df-rp 10038 df-fz 10395 df-fzo 10533 df-seqfrec 10868 df-exp 10959 df-ihash 11198 df-cj 11590 df-re 11591 df-im 11592 df-rsqrt 11747 df-abs 11748 df-clim 12028

This theorem is referenced by: fsum3 12137

W3C validator