Theorem prodmodc 11352

Description: A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017.) (Modified by Jim Kingdon, 14-Apr-2024.)

Hypotheses

Ref	Expression
prodmo.1	⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
prodmo.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
prodmodc.3	⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))

Assertion

Ref	Expression
prodmodc	⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))))

Distinct variable groups:   𝐴,𝑓,𝑗,𝑘,𝑚,𝑥   𝐵,𝑓,𝑗,𝑚   𝑓,𝐹,𝑘,𝑚,𝑥   𝑗,𝐺,𝑥   𝜑,𝑓,𝑘,𝑚,𝑥   𝑥,𝑛   𝑥,𝑦

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

Proof of Theorem prodmodc

Dummy variables 𝑎 𝑔 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 518	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → 𝐴 ⊆ (ℤ≥‘𝑚))
2		simplr 519	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)
3		simprr 521	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → seq𝑚( · , 𝐹) ⇝ 𝑥)
4	1, 2, 3	3jca 1161	. . . . . . 7 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))
5	4	reximi 2529	. . . . . 6 ⊢ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))
6		simpll 518	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → 𝐴 ⊆ (ℤ≥‘𝑚))
7		simplr 519	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)
8		simprr 521	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → seq𝑚( · , 𝐹) ⇝ 𝑧)
9	6, 7, 8	3jca 1161	. . . . . . 7 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))
10	9	reximi 2529	. . . . . 6 ⊢ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))
11		fveq2 5421	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑤 → (ℤ≥‘𝑚) = (ℤ≥‘𝑤))
12	11	sseq2d 3127	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐴 ⊆ (ℤ≥‘𝑤)))
13	11	raleqdv 2632	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴))
14		seqeq1 10226	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑤 → seq𝑚( · , 𝐹) = seq𝑤( · , 𝐹))
15	14	breq1d 3939	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (seq𝑚( · , 𝐹) ⇝ 𝑧 ↔ seq𝑤( · , 𝐹) ⇝ 𝑧))
16	12, 13, 15	3anbi123d 1290	. . . . . . . . . 10 ⊢ (𝑚 = 𝑤 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ↔ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
17	16	cbvrexvw 2659	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ↔ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))
18	17	anbi2i 452	. . . . . . . 8 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
19		reeanv 2600	. . . . . . . 8 ⊢ (∃𝑚 ∈ ℤ ∃𝑤 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
20	18, 19	bitr4i 186	. . . . . . 7 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ↔ ∃𝑚 ∈ ℤ ∃𝑤 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
21		simprl3 1028	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → seq𝑚( · , 𝐹) ⇝ 𝑥)
22	21	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑚( · , 𝐹) ⇝ 𝑥)
23		prodmo.1	. . . . . . . . . . . . 13 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
24		prodmo.2	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
25	24	adantlr 468	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
26		simprll 526	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑚 ∈ ℤ)
27		simprlr 527	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑤 ∈ ℤ)
28		simprl1 1026	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → 𝐴 ⊆ (ℤ≥‘𝑚))
29	28	adantl 275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝐴 ⊆ (ℤ≥‘𝑚))
30		simprr1 1029	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → 𝐴 ⊆ (ℤ≥‘𝑤))
31	30	adantl 275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝐴 ⊆ (ℤ≥‘𝑤))
32		eleq1w 2200	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
33	32	dcbid 823	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴))
34		simprl2 1027	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)
35	34	ad2antlr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)
36		simpr 109	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → 𝑘 ∈ (ℤ≥‘𝑚))
37	33, 35, 36	rspcdva 2794	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → DECID 𝑘 ∈ 𝐴)
38		simprr2 1030	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴)
39	38	ad2antlr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ≥‘𝑤)) → ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴)
40		simpr 109	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ≥‘𝑤)) → 𝑘 ∈ (ℤ≥‘𝑤))
41	33, 39, 40	rspcdva 2794	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ≥‘𝑤)) → DECID 𝑘 ∈ 𝐴)
42	23, 25, 26, 27, 29, 31, 37, 41	prodrbdc 11348	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → (seq𝑚( · , 𝐹) ⇝ 𝑥 ↔ seq𝑤( · , 𝐹) ⇝ 𝑥))
43	22, 42	mpbid 146	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑤( · , 𝐹) ⇝ 𝑥)
44		simprr3 1031	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → seq𝑤( · , 𝐹) ⇝ 𝑧)
45	44	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑤( · , 𝐹) ⇝ 𝑧)
46		climuni 11067	. . . . . . . . . . 11 ⊢ ((seq𝑤( · , 𝐹) ⇝ 𝑥 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧) → 𝑥 = 𝑧)
47	43, 45, 46	syl2anc 408	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑥 = 𝑧)
48	47	expcom 115	. . . . . . . . 9 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → (𝜑 → 𝑥 = 𝑧))
49	48	ex 114	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) → (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)) → (𝜑 → 𝑥 = 𝑧)))
50	49	rexlimivv 2555	. . . . . . 7 ⊢ (∃𝑚 ∈ ℤ ∃𝑤 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)) → (𝜑 → 𝑥 = 𝑧))
51	20, 50	sylbi 120	. . . . . 6 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (𝜑 → 𝑥 = 𝑧))
52	5, 10, 51	syl2an 287	. . . . 5 ⊢ ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (𝜑 → 𝑥 = 𝑧))
53		prodmodc.3	. . . . . . . . . 10 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
54	23, 24, 53	prodmodclem2 11351	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) → 𝑧 = 𝑥))
55		equcomi 1680	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → 𝑥 = 𝑧)
56	54, 55	syl6 33	. . . . . . . 8 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧))
57	56	expimpd 360	. . . . . . 7 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) → 𝑥 = 𝑧))
58	57	com12 30	. . . . . 6 ⊢ ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) → (𝜑 → 𝑥 = 𝑧))
59	58	ancoms 266	. . . . 5 ⊢ ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (𝜑 → 𝑥 = 𝑧))
60	23, 24, 53	prodmodclem2 11351	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧))
61	60	expimpd 360	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))) → 𝑥 = 𝑧))
62	61	com12 30	. . . . 5 ⊢ ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))) → (𝜑 → 𝑥 = 𝑧))
63		reeanv 2600	. . . . . . . 8 ⊢ (∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑤 ∈ ℕ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
64		exdistrv 1882	. . . . . . . . 9 ⊢ (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) ↔ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
65	64	2rexbii 2444	. . . . . . . 8 ⊢ (∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ ∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) ↔ ∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
66		oveq2 5782	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑤 → (1...𝑚) = (1...𝑤))
67	66	f1oeq2d 5363	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑤 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑤)–1-1-onto→𝐴))
68		fveq2 5421	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑤 → (seq1( · , 𝐺)‘𝑚) = (seq1( · , 𝐺)‘𝑤))
69	68	eqeq2d 2151	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑤 → (𝑧 = (seq1( · , 𝐺)‘𝑚) ↔ 𝑧 = (seq1( · , 𝐺)‘𝑤)))
70	67, 69	anbi12d 464	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑤 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤))))
71	70	exbidv 1797	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤))))
72		f1oeq1 5356	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓:(1...𝑤)–1-1-onto→𝐴 ↔ 𝑔:(1...𝑤)–1-1-onto→𝐴))
73		fveq1 5420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑗) = (𝑔‘𝑗))
74	73	csbeq1d 3010	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑔 → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑗) / 𝑘⦌𝐵)
75	74	ifeq1d 3489	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1))
76	75	mpteq2dv 4019	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))
77	53, 76	syl5eq 2184	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))
78	77	seqeq3d 10231	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → seq1( · , 𝐺) = seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1))))
79	78	fveq1d 5423	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (seq1( · , 𝐺)‘𝑤) = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))
80	79	eqeq2d 2151	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑧 = (seq1( · , 𝐺)‘𝑤) ↔ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
81	72, 80	anbi12d 464	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤)) ↔ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
82	81	cbvexvw 1892	. . . . . . . . . . 11 ⊢ (∃𝑓(𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤)) ↔ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
83	71, 82	syl6bb 195	. . . . . . . . . 10 ⊢ (𝑚 = 𝑤 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
84	83	cbvrexvw 2659	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑤 ∈ ℕ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
85	84	anbi2i 452	. . . . . . . 8 ⊢ ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑤 ∈ ℕ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
86	63, 65, 85	3bitr4i 211	. . . . . . 7 ⊢ (∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ ∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
87		an4 575	. . . . . . . . . 10 ⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) ↔ ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴) ∧ (𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
88	24	ad4ant14 505	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
89		breq1 3932	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑎 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑎 ≤ (♯‘𝐴)))
90		fveq2 5421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑎 → (𝑓‘𝑗) = (𝑓‘𝑎))
91	90	csbeq1d 3010	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑎 → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑎) / 𝑘⦌𝐵)
92	89, 91	ifbieq1d 3494	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑎 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 1))
93	92	cbvmptv 4024	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 1))
94	53, 93	eqtri 2160	. . . . . . . . . . . . 13 ⊢ 𝐺 = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 1))
95		fveq2 5421	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑎 → (𝑔‘𝑗) = (𝑔‘𝑎))
96	95	csbeq1d 3010	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑎 → ⦋(𝑔‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑎) / 𝑘⦌𝐵)
97	89, 96	ifbieq1d 3494	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑎 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 1))
98	97	cbvmptv 4024	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 1))
99		simplr 519	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ))
100		simprl 520	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
101		simprr 521	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → 𝑔:(1...𝑤)–1-1-onto→𝐴)
102	23, 88, 94, 98, 99, 100, 101	prodmodclem3 11349	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → (seq1( · , 𝐺)‘𝑚) = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))
103		eqeq12 2152	. . . . . . . . . . . 12 ⊢ ((𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)) → (𝑥 = 𝑧 ↔ (seq1( · , 𝐺)‘𝑚) = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
104	102, 103	syl5ibrcom 156	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → ((𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)) → 𝑥 = 𝑧))
105	104	expimpd 360	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴) ∧ (𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) → 𝑥 = 𝑧))
106	87, 105	syl5bi 151	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) → 𝑥 = 𝑧))
107	106	exlimdvv 1869	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) → 𝑥 = 𝑧))
108	107	rexlimdvva 2557	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ ∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) → 𝑥 = 𝑧))
109	86, 108	syl5bir 152	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))) → 𝑥 = 𝑧))
110	109	com12 30	. . . . 5 ⊢ ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))) → (𝜑 → 𝑥 = 𝑧))
111	52, 59, 62, 110	ccase 948	. . . 4 ⊢ (((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)))) → (𝜑 → 𝑥 = 𝑧))
112	111	com12 30	. . 3 ⊢ (𝜑 → (((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)))) → 𝑥 = 𝑧))
113	112	alrimivv 1847	. 2 ⊢ (𝜑 → ∀𝑥∀𝑧(((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)))) → 𝑥 = 𝑧))
114		breq2 3933	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (seq𝑚( · , 𝐹) ⇝ 𝑥 ↔ seq𝑚( · , 𝐹) ⇝ 𝑧))
115	114	anbi2d 459	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)))
116	115	anbi2d 459	. . . . 5 ⊢ (𝑥 = 𝑧 → (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))))
117	116	rexbidv 2438	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))))
118		eqeq1 2146	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 = (seq1( · , 𝐺)‘𝑚) ↔ 𝑧 = (seq1( · , 𝐺)‘𝑚)))
119	118	anbi2d 459	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
120	119	exbidv 1797	. . . . 5 ⊢ (𝑥 = 𝑧 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
121	120	rexbidv 2438	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
122	117, 121	orbi12d 782	. . 3 ⊢ (𝑥 = 𝑧 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)))))
123	122	mo4 2060	. 2 ⊢ (∃*𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ↔ ∀𝑥∀𝑧(((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)))) → 𝑥 = 𝑧))
124	113, 123	sylibr 133	1 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))))

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 697  DECID wdc 819   ∧ w3a 962  ∀wal 1329   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∃*wmo 2000  ∀wral 2416  ∃wrex 2417  ⦋csb 3003   ⊆ wss 3071  ifcif 3474   class class class wbr 3929   ↦ cmpt 3989  –1-1-onto→wf1o 5122  ‘cfv 5123  (class class class)co 5774  ℂcc 7623  0cc0 7625  1c1 7626   · cmul 7630   ≤ cle 7806   # cap 8348  ℕcn 8725  ℤcz 9059  ℤ_≥cuz 9331  ...cfz 9795  seqcseq 10223  ♯chash 10526   ⇝ cli 11052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7716  ax-resscn 7717  ax-1cn 7718  ax-1re 7719  ax-icn 7720  ax-addcl 7721  ax-addrcl 7722  ax-mulcl 7723  ax-mulrcl 7724  ax-addcom 7725  ax-mulcom 7726  ax-addass 7727  ax-mulass 7728  ax-distr 7729  ax-i2m1 7730  ax-0lt1 7731  ax-1rid 7732  ax-0id 7733  ax-rnegex 7734  ax-precex 7735  ax-cnre 7736  ax-pre-ltirr 7737  ax-pre-ltwlin 7738  ax-pre-lttrn 7739  ax-pre-apti 7740  ax-pre-ltadd 7741  ax-pre-mulgt0 7742  ax-pre-mulext 7743  ax-arch 7744  ax-caucvg 7745

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-frec 6288  df-1o 6313  df-oadd 6317  df-er 6429  df-en 6635  df-dom 6636  df-fin 6637  df-pnf 7807  df-mnf 7808  df-xr 7809  df-ltxr 7810  df-le 7811  df-sub 7940  df-neg 7941  df-reap 8342  df-ap 8349  df-div 8438  df-inn 8726  df-2 8784  df-3 8785  df-4 8786  df-n0 8983  df-z 9060  df-uz 9332  df-q 9417  df-rp 9447  df-fz 9796  df-fzo 9925  df-seqfrec 10224  df-exp 10298  df-ihash 10527  df-cj 10619  df-re 10620  df-im 10621  df-rsqrt 10775  df-abs 10776  df-clim 11053

This theorem is referenced by: (None)