prodmodc - Intuitionistic Logic Explorer

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

Theorem prodmodc 11570

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 527	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
2		simplr 528	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
3		simprr 531	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → seq𝑚( · , 𝐹) ⇝ 𝑥)
4	1, 2, 3	3jca 1177	. . . . . . 7 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))
5	4	reximi 2574	. . . . . 6 ⊢ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))
6		simpll 527	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
7		simplr 528	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
8		simprr 531	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → seq𝑚( · , 𝐹) ⇝ 𝑧)
9	6, 7, 8	3jca 1177	. . . . . . 7 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))
10	9	reximi 2574	. . . . . 6 ⊢ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))
11		fveq2 5511	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑤 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑤))
12	11	sseq2d 3185	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ (ℤ_≥‘𝑤)))
13	11	raleqdv 2678	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴))
14		seqeq1 10434	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑤 → seq𝑚( · , 𝐹) = seq𝑤( · , 𝐹))
15	14	breq1d 4010	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (seq𝑚( · , 𝐹) ⇝ 𝑧 ↔ seq𝑤( · , 𝐹) ⇝ 𝑧))
16	12, 13, 15	3anbi123d 1312	. . . . . . . . . 10 ⊢ (𝑚 = 𝑤 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ↔ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
17	16	cbvrexvw 2708	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ↔ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))
18	17	anbi2i 457	. . . . . . . 8 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
19		reeanv 2646	. . . . . . . 8 ⊢ (∃𝑚 ∈ ℤ ∃𝑤 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
20	18, 19	bitr4i 187	. . . . . . 7 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ↔ ∃𝑚 ∈ ℤ ∃𝑤 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
21		simprl3 1044	. . . . . . . . . . . . 13 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → seq𝑚( · , 𝐹) ⇝ 𝑥)
22	21	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑚( · , 𝐹) ⇝ 𝑥)
23		prodmo.1	. . . . . . . . . . . . 13 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
24		prodmo.2	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
25	24	adantlr 477	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
26		simprll 537	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑚 ∈ ℤ)
27		simprlr 538	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑤 ∈ ℤ)
28		simprl1 1042	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → 𝐴 ⊆ (ℤ_≥‘𝑚))
29	28	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝐴 ⊆ (ℤ_≥‘𝑚))
30		simprr1 1045	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → 𝐴 ⊆ (ℤ_≥‘𝑤))
31	30	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝐴 ⊆ (ℤ_≥‘𝑤))
32		eleq1w 2238	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
33	32	dcbid 838	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴))
34		simprl2 1043	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
35	34	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
36		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → 𝑘 ∈ (ℤ_≥‘𝑚))
37	33, 35, 36	rspcdva 2846	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → DECID 𝑘 ∈ 𝐴)
38		simprr2 1046	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴)
39	38	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑤)) → ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴)
40		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑤)) → 𝑘 ∈ (ℤ_≥‘𝑤))
41	33, 39, 40	rspcdva 2846	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑤)) → DECID 𝑘 ∈ 𝐴)
42	23, 25, 26, 27, 29, 31, 37, 41	prodrbdc 11566	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → (seq𝑚( · , 𝐹) ⇝ 𝑥 ↔ seq𝑤( · , 𝐹) ⇝ 𝑥))
43	22, 42	mpbid 147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑤( · , 𝐹) ⇝ 𝑥)
44		simprr3 1047	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → seq𝑤( · , 𝐹) ⇝ 𝑧)
45	44	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑤( · , 𝐹) ⇝ 𝑧)
46		climuni 11285	. . . . . . . . . . 11 ⊢ ((seq𝑤( · , 𝐹) ⇝ 𝑥 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧) → 𝑥 = 𝑧)
47	43, 45, 46	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑥 = 𝑧)
48	47	expcom 116	. . . . . . . . 9 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → (𝜑 → 𝑥 = 𝑧))
49	48	ex 115	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) → (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)) → (𝜑 → 𝑥 = 𝑧)))
50	49	rexlimivv 2600	. . . . . . 7 ⊢ (∃𝑚 ∈ ℤ ∃𝑤 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)) → (𝜑 → 𝑥 = 𝑧))
51	20, 50	sylbi 121	. . . . . 6 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (𝜑 → 𝑥 = 𝑧))
52	5, 10, 51	syl2an 289	. . . . 5 ⊢ ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (𝜑 → 𝑥 = 𝑧))
53		prodmodc.3	. . . . . . . . . 10 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
54	23, 24, 53	prodmodclem2 11569	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) → 𝑧 = 𝑥))
55		equcomi 1704	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → 𝑥 = 𝑧)
56	54, 55	syl6 33	. . . . . . . 8 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧))
57	56	expimpd 363	. . . . . . 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 268	. . . . 5 ⊢ ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (𝜑 → 𝑥 = 𝑧))
60	23, 24, 53	prodmodclem2 11569	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧))
61	60	expimpd 363	. . . . . 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 2646	. . . . . . . 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 1910	. . . . . . . . 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 2486	. . . . . . . 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 5877	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑤 → (1...𝑚) = (1...𝑤))
67	66	f1oeq2d 5453	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑤 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑤)–1-1-onto→𝐴))
68		fveq2 5511	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑤 → (seq1( · , 𝐺)‘𝑚) = (seq1( · , 𝐺)‘𝑤))
69	68	eqeq2d 2189	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑤 → (𝑧 = (seq1( · , 𝐺)‘𝑚) ↔ 𝑧 = (seq1( · , 𝐺)‘𝑤)))
70	67, 69	anbi12d 473	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑤 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤))))
71	70	exbidv 1825	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤))))
72		f1oeq1 5445	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓:(1...𝑤)–1-1-onto→𝐴 ↔ 𝑔:(1...𝑤)–1-1-onto→𝐴))
73		fveq1 5510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑗) = (𝑔‘𝑗))
74	73	csbeq1d 3064	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑔 → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑗) / 𝑘⦌𝐵)
75	74	ifeq1d 3551	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1))
76	75	mpteq2dv 4091	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))
77	53, 76	eqtrid 2222	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))
78	77	seqeq3d 10439	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → seq1( · , 𝐺) = seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1))))
79	78	fveq1d 5513	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (seq1( · , 𝐺)‘𝑤) = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))
80	79	eqeq2d 2189	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑧 = (seq1( · , 𝐺)‘𝑤) ↔ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
81	72, 80	anbi12d 473	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤)) ↔ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
82	81	cbvexvw 1920	. . . . . . . . . . 11 ⊢ (∃𝑓(𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤)) ↔ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
83	71, 82	bitrdi 196	. . . . . . . . . 10 ⊢ (𝑚 = 𝑤 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
84	83	cbvrexvw 2708	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑤 ∈ ℕ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
85	84	anbi2i 457	. . . . . . . 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 212	. . . . . . 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 586	. . . . . . . . . 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 514	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
89		breq1 4003	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑎 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑎 ≤ (♯‘𝐴)))
90		fveq2 5511	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑎 → (𝑓‘𝑗) = (𝑓‘𝑎))
91	90	csbeq1d 3064	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑎 → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑎) / 𝑘⦌𝐵)
92	89, 91	ifbieq1d 3556	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑎 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 1))
93	92	cbvmptv 4096	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 1))
94	53, 93	eqtri 2198	. . . . . . . . . . . . 13 ⊢ 𝐺 = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 1))
95		fveq2 5511	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑎 → (𝑔‘𝑗) = (𝑔‘𝑎))
96	95	csbeq1d 3064	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑎 → ⦋(𝑔‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑎) / 𝑘⦌𝐵)
97	89, 96	ifbieq1d 3556	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑎 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 1))
98	97	cbvmptv 4096	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 1))
99		simplr 528	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ))
100		simprl 529	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
101		simprr 531	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → 𝑔:(1...𝑤)–1-1-onto→𝐴)
102	23, 88, 94, 98, 99, 100, 101	prodmodclem3 11567	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → (seq1( · , 𝐺)‘𝑚) = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))
103		eqeq12 2190	. . . . . . . . . . . 12 ⊢ ((𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)) → (𝑥 = 𝑧 ↔ (seq1( · , 𝐺)‘𝑚) = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
104	102, 103	syl5ibrcom 157	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → ((𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)) → 𝑥 = 𝑧))
105	104	expimpd 363	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴) ∧ (𝑥 = (seq1( · , 𝐺)‘𝑚) ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) → 𝑥 = 𝑧))
106	87, 105	biimtrid 152	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) → 𝑥 = 𝑧))
107	106	exlimdvv 1897	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) → 𝑥 = 𝑧))
108	107	rexlimdvva 2602	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑤 ∈ ℕ ∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) → 𝑥 = 𝑧))
109	86, 108	biimtrrid 153	. . . . . 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 964	. . . 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 1875	. 2 ⊢ (𝜑 → ∀𝑥∀𝑧(((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)))) → 𝑥 = 𝑧))
114		breq2 4004	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (seq𝑚( · , 𝐹) ⇝ 𝑥 ↔ seq𝑚( · , 𝐹) ⇝ 𝑧))
115	114	anbi2d 464	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)))
116	115	anbi2d 464	. . . . 5 ⊢ (𝑥 = 𝑧 → (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))))
117	116	rexbidv 2478	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))))
118		eqeq1 2184	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 = (seq1( · , 𝐺)‘𝑚) ↔ 𝑧 = (seq1( · , 𝐺)‘𝑚)))
119	118	anbi2d 464	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
120	119	exbidv 1825	. . . . 5 ⊢ (𝑥 = 𝑧 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
121	120	rexbidv 2478	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
122	117, 121	orbi12d 793	. . 3 ⊢ (𝑥 = 𝑧 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)))))
123	122	mo4 2087	. 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 134	1 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∨ wo 708 DECID wdc 834 ∧ w3a 978 ∀wal 1351 = wceq 1353 ∃wex 1492 ∃*wmo 2027 ∈ wcel 2148 ∀wral 2455 ∃wrex 2456 ⦋csb 3057 ⊆ wss 3129 ifcif 3534 class class class wbr 4000 ↦ cmpt 4061 –1-1-onto→wf1o 5211 ‘cfv 5212 (class class class)co 5869 ℂcc 7800 0cc0 7802 1c1 7803 · cmul 7807 ≤ cle 7983 # cap 8528 ℕcn 8908 ℤcz 9242 ℤ_≥cuz 9517 ...cfz 9995 seqcseq 10431 ♯chash 10739 ⇝ cli 11270

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-iinf 4584 ax-cnex 7893 ax-resscn 7894 ax-1cn 7895 ax-1re 7896 ax-icn 7897 ax-addcl 7898 ax-addrcl 7899 ax-mulcl 7900 ax-mulrcl 7901 ax-addcom 7902 ax-mulcom 7903 ax-addass 7904 ax-mulass 7905 ax-distr 7906 ax-i2m1 7907 ax-0lt1 7908 ax-1rid 7909 ax-0id 7910 ax-rnegex 7911 ax-precex 7912 ax-cnre 7913 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-apti 7917 ax-pre-ltadd 7918 ax-pre-mulgt0 7919 ax-pre-mulext 7920 ax-arch 7921 ax-caucvg 7922

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4290 df-po 4293 df-iso 4294 df-iord 4363 df-on 4365 df-ilim 4366 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-isom 5221 df-riota 5825 df-ov 5872 df-oprab 5873 df-mpo 5874 df-1st 6135 df-2nd 6136 df-recs 6300 df-irdg 6365 df-frec 6386 df-1o 6411 df-oadd 6415 df-er 6529 df-en 6735 df-dom 6736 df-fin 6737 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988 df-sub 8120 df-neg 8121 df-reap 8522 df-ap 8529 df-div 8619 df-inn 8909 df-2 8967 df-3 8968 df-4 8969 df-n0 9166 df-z 9243 df-uz 9518 df-q 9609 df-rp 9641 df-fz 9996 df-fzo 10129 df-seqfrec 10432 df-exp 10506 df-ihash 10740 df-cj 10835 df-re 10836 df-im 10837 df-rsqrt 10991 df-abs 10992 df-clim 11271

This theorem is referenced by: fprodseq 11575

W3C validator