summodc - Intuitionistic Logic Explorer

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

Theorem summodc 11967

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 5642	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑛))
2	1	sseq2d 3256	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ (ℤ_≥‘𝑛)))
3	1	raleqdv 2735	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴))
4		seqeq1 10718	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → seq𝑚( + , 𝐹) = seq𝑛( + , 𝐹))
5	4	breq1d 4099	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (seq𝑚( + , 𝐹) ⇝ 𝑦 ↔ seq𝑛( + , 𝐹) ⇝ 𝑦))
6	2, 3, 5	3anbi123d 1348	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
7	6	cbvrexv 2767	. . . . . . 7 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))
8		reeanv 2702	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
9		simprl3 1070	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑚( + , 𝐹) ⇝ 𝑥)
10		isummo.1	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
11		simpll 527	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝜑)
12		isummo.2	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
13	11, 12	sylan 283	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
14		simplrl 537	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑚 ∈ ℤ)
15		simplrr 538	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑛 ∈ ℤ)
16		simprl1 1068	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ_≥‘𝑚))
17		simprr1 1071	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ_≥‘𝑛))
18		eleq1w 2291	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
19	18	dcbid 845	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴))
20		simprl2 1069	. . . . . . . . . . . . . . . 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 2914	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → DECID 𝑘 ∈ 𝐴)
24		simprr2 1072	. . . . . . . . . . . . . . . 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 2914	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ (ℤ_≥‘𝑛)) → DECID 𝑘 ∈ 𝐴)
28	10, 13, 14, 15, 16, 17, 23, 27	sumrbdc 11963	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑛( + , 𝐹) ⇝ 𝑥))
29	9, 28	mpbid 147	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑥)
30		simprr3 1073	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑦)
31		climuni 11876	. . . . . . . . . . . 12 ⊢ ((seq𝑛( + , 𝐹) ⇝ 𝑥 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦)
32	29, 30, 31	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑥 = 𝑦)
33	32	exp31 364	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑛) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑛)DECID 𝑗 ∈ 𝐴 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦)))
34	33	rexlimdvv 2656	. . . . . . . . 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 11966	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
40	37, 39	jaod 724	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
41	10, 12, 38	summodclem2 11966	. . . . . . . 8 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑦 = 𝑥))
42		equcom 1753	. . . . . . . 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 6031	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
46		f1oeq2 5575	. . . . . . . . . . . 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 5642	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘𝑛))
49	48	eqeq2d 2242	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑦 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑛)))
50	47, 49	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛))))
51	50	exbidv 1872	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛))))
52		f1oeq1 5574	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑓:(1...𝑛)–1-1-onto→𝐴 ↔ 𝑔:(1...𝑛)–1-1-onto→𝐴))
53		breq1 4092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑎 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑎 ≤ (♯‘𝐴)))
54		fveq2 5642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑎 → (𝑓‘𝑛) = (𝑓‘𝑎))
55	54	csbeq1d 3133	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑎 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑎) / 𝑘⦌𝐵)
56	53, 55	ifbieq1d 3629	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑎 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 0))
57	56	cbvmptv 4186	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 0))
58		fveq1 5641	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑎) = (𝑔‘𝑎))
59	58	csbeq1d 3133	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → ⦋(𝑓‘𝑎) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑎) / 𝑘⦌𝐵)
60	59	ifeq1d 3624	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 0) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))
61	60	mpteq2dv 4181	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))
62	57, 61	eqtrid 2275	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))
63	38, 62	eqtrid 2275	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → 𝐺 = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))
64	63	seqeq3d 10723	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → seq1( + , 𝐺) = seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))))
65	64	fveq1d 5644	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (seq1( + , 𝐺)‘𝑛) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))
66	65	eqeq2d 2242	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑦 = (seq1( + , 𝐺)‘𝑛) ↔ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)))
67	52, 66	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))))
68	67	cbvexv 1966	. . . . . . . . 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 2767	. . . . . . 7 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)))
71		reeanv 2702	. . . . . . . . 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 1984	. . . . . . . . . . 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 588	. . . . . . . . . . . . 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 9511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 1 ∈ ℤ)
75		simplrr 538	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑛 ∈ ℕ)
76	75	nnzd 9606	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑛 ∈ ℤ)
77	74, 76	fzfigd 10699	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (1...𝑛) ∈ Fin)
78		simprr 533	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑔:(1...𝑛)–1-1-onto→𝐴)
79	77, 78	fihasheqf1od 11057	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘(1...𝑛)) = (♯‘𝐴))
80	75	nnnn0d 9460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑛 ∈ ℕ₀)
81		hashfz1 11051	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ℕ₀ → (♯‘(1...𝑛)) = 𝑛)
82	80, 81	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘(1...𝑛)) = 𝑛)
83	79, 82	eqtr3d 2265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘𝐴) = 𝑛)
84	83	breq2d 4101	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (𝑎 ≤ (♯‘𝐴) ↔ 𝑎 ≤ 𝑛))
85	84	ifbid 3628	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0) = if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))
86	85	mpteq2dv 4181	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))
87	86	seqeq3d 10723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0))))
88	87	fveq1d 5644	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))
89	88	eqeq2d 2242	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛) ↔ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)))
90	89	anbi2d 464	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛)) ↔ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))))
91		simplrl 537	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑚 ∈ ℕ)
92	91	nnnn0d 9460	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑚 ∈ ℕ₀)
93		hashfz1 11051	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
94	92, 93	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘(1...𝑚)) = 𝑚)
95	91	nnzd 9606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑚 ∈ ℤ)
96	74, 95	fzfigd 10699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (1...𝑚) ∈ Fin)
97		simprl 531	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
98	96, 97	fihasheqf1od 11057	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (♯‘(1...𝑚)) = (♯‘𝐴))
99	94, 98	eqtr3d 2265	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑚 = (♯‘𝐴))
100	99	fveq2d 5646	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘(♯‘𝐴)))
101		simpll 527	. . . . . . . . . . . . . . . . . . 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 2308	. . . . . . . . . . . . . . . . . . 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 6039	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (1...𝑚) = (1...(♯‘𝐴)))
106		f1oeq2 5575	. . . . . . . . . . . . . . . . . . . 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 4092	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
110		fveq2 5642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
111	110	csbeq1d 3133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
112	109, 111	ifbieq1d 3629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 0))
113	112	cbvmptv 4186	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 0))
114	38, 113	eqtri 2251	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 0))
115		breq1 4092	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑗 → (𝑎 ≤ 𝑛 ↔ 𝑗 ≤ 𝑛))
116		fveq2 5642	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑗 → (𝑔‘𝑎) = (𝑔‘𝑗))
117	116	csbeq1d 3133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑗 → ⦋(𝑔‘𝑎) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑗) / 𝑘⦌𝐵)
118	115, 117	ifbieq1d 3629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑗 → if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0) = if(𝑗 ≤ 𝑛, ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 0))
119	118	cbvmptv 4186	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ 𝑛, ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 0))
120	10, 102, 104, 108, 78, 114, 119	summodclem3 11964	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))
121	100, 120	eqtrd 2263	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑎 ∈ ℕ ↦ if(𝑎 ≤ 𝑛, ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 0)))‘𝑛))
122		eqeq12 2243	. . . . . . . . . . . . . . . 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 1945	. . . . . . . . . . 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 2657	. . . . . . . . 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 724	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
134	40, 133	jaodan 804	. . . 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 1922	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
137		breq2 4093	. . . . . 6 ⊢ (𝑥 = 𝑦 → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑚( + , 𝐹) ⇝ 𝑦))
138	137	3anbi3d 1354	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
139	138	rexbidv 2532	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
140		eqeq1 2237	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑚)))
141	140	anbi2d 464	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
142	141	exbidv 1872	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
143	142	rexbidv 2532	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
144	139, 143	orbi12d 800	. . 3 ⊢ (𝑥 = 𝑦 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))))
145	144	mo4 2140	. 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 715 DECID wdc 841 ∧ w3a 1004 ∀wal 1395 = wceq 1397 ∃wex 1540 ∃*wmo 2079 ∈ wcel 2201 ∀wral 2509 ∃wrex 2510 ⦋csb 3126 ⊆ wss 3199 ifcif 3604 class class class wbr 4089 ↦ cmpt 4151 –1-1-onto→wf1o 5327 ‘cfv 5328 (class class class)co 6023 ℂcc 8035 0cc0 8037 1c1 8038 + caddc 8040 ≤ cle 8220 ℕcn 9148 ℕ₀cn0 9407 ℤcz 9484 ℤ_≥cuz 9760 ...cfz 10248 seqcseq 10715 ♯chash 11043 ⇝ cli 11861

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2203 ax-14 2204 ax-ext 2212 ax-coll 4205 ax-sep 4208 ax-nul 4216 ax-pow 4266 ax-pr 4301 ax-un 4532 ax-setind 4637 ax-iinf 4688 ax-cnex 8128 ax-resscn 8129 ax-1cn 8130 ax-1re 8131 ax-icn 8132 ax-addcl 8133 ax-addrcl 8134 ax-mulcl 8135 ax-mulrcl 8136 ax-addcom 8137 ax-mulcom 8138 ax-addass 8139 ax-mulass 8140 ax-distr 8141 ax-i2m1 8142 ax-0lt1 8143 ax-1rid 8144 ax-0id 8145 ax-rnegex 8146 ax-precex 8147 ax-cnre 8148 ax-pre-ltirr 8149 ax-pre-ltwlin 8150 ax-pre-lttrn 8151 ax-pre-apti 8152 ax-pre-ltadd 8153 ax-pre-mulgt0 8154 ax-pre-mulext 8155 ax-arch 8156 ax-caucvg 8157

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1810 df-eu 2081 df-mo 2082 df-clab 2217 df-cleq 2223 df-clel 2226 df-nfc 2362 df-ne 2402 df-nel 2497 df-ral 2514 df-rex 2515 df-reu 2516 df-rmo 2517 df-rab 2518 df-v 2803 df-sbc 3031 df-csb 3127 df-dif 3201 df-un 3203 df-in 3205 df-ss 3212 df-nul 3494 df-if 3605 df-pw 3655 df-sn 3676 df-pr 3677 df-op 3679 df-uni 3895 df-int 3930 df-iun 3973 df-br 4090 df-opab 4152 df-mpt 4153 df-tr 4189 df-id 4392 df-po 4395 df-iso 4396 df-iord 4465 df-on 4467 df-ilim 4468 df-suc 4470 df-iom 4691 df-xp 4733 df-rel 4734 df-cnv 4735 df-co 4736 df-dm 4737 df-rn 4738 df-res 4739 df-ima 4740 df-iota 5288 df-fun 5330 df-fn 5331 df-f 5332 df-f1 5333 df-fo 5334 df-f1o 5335 df-fv 5336 df-isom 5337 df-riota 5976 df-ov 6026 df-oprab 6027 df-mpo 6028 df-1st 6308 df-2nd 6309 df-recs 6476 df-irdg 6541 df-frec 6562 df-1o 6587 df-oadd 6591 df-er 6707 df-en 6915 df-dom 6916 df-fin 6917 df-pnf 8221 df-mnf 8222 df-xr 8223 df-ltxr 8224 df-le 8225 df-sub 8357 df-neg 8358 df-reap 8760 df-ap 8767 df-div 8858 df-inn 9149 df-2 9207 df-3 9208 df-4 9209 df-n0 9408 df-z 9485 df-uz 9761 df-q 9859 df-rp 9894 df-fz 10249 df-fzo 10383 df-seqfrec 10716 df-exp 10807 df-ihash 11044 df-cj 11425 df-re 11426 df-im 11427 df-rsqrt 11581 df-abs 11582 df-clim 11862

This theorem is referenced by: fsum3 11971

W3C validator