prodmodc - Intuitionistic Logic Explorer

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

Theorem prodmodc 11379

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 519	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
2		simplr 520	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
3		simprr 522	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → seq𝑚( · , 𝐹) ⇝ 𝑥)
4	1, 2, 3	3jca 1162	. . . . . . 7 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))
5	4	reximi 2532	. . . . . 6 ⊢ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))
6		simpll 519	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
7		simplr 520	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
8		simprr 522	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → seq𝑚( · , 𝐹) ⇝ 𝑧)
9	6, 7, 8	3jca 1162	. . . . . . 7 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))
10	9	reximi 2532	. . . . . 6 ⊢ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))
11		fveq2 5429	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑤 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑤))
12	11	sseq2d 3132	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ (ℤ_≥‘𝑤)))
13	11	raleqdv 2635	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴))
14		seqeq1 10252	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑤 → seq𝑚( · , 𝐹) = seq𝑤( · , 𝐹))
15	14	breq1d 3947	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (seq𝑚( · , 𝐹) ⇝ 𝑧 ↔ seq𝑤( · , 𝐹) ⇝ 𝑧))
16	12, 13, 15	3anbi123d 1291	. . . . . . . . . 10 ⊢ (𝑚 = 𝑤 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ↔ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
17	16	cbvrexvw 2662	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧) ↔ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))
18	17	anbi2i 453	. . . . . . . 8 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ ∃𝑤 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))
19		reeanv 2603	. . . . . . . 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 1029	. . . . . . . . . . . . 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 469	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
26		simprll 527	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑚 ∈ ℤ)
27		simprlr 528	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝑤 ∈ ℤ)
28		simprl1 1027	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → 𝐴 ⊆ (ℤ_≥‘𝑚))
29	28	adantl 275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝐴 ⊆ (ℤ_≥‘𝑚))
30		simprr1 1030	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → 𝐴 ⊆ (ℤ_≥‘𝑤))
31	30	adantl 275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → 𝐴 ⊆ (ℤ_≥‘𝑤))
32		eleq1w 2201	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
33	32	dcbid 824	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴))
34		simprl2 1028	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
35	34	ad2antlr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
36		simpr 109	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → 𝑘 ∈ (ℤ_≥‘𝑚))
37	33, 35, 36	rspcdva 2798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑚)) → DECID 𝑘 ∈ 𝐴)
38		simprr2 1031	. . . . . . . . . . . . . . 15 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴)
39	38	ad2antlr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑤)) → ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴)
40		simpr 109	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑤)) → 𝑘 ∈ (ℤ_≥‘𝑤))
41	33, 39, 40	rspcdva 2798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) ∧ 𝑘 ∈ (ℤ_≥‘𝑤)) → DECID 𝑘 ∈ 𝐴)
42	23, 25, 26, 27, 29, 31, 37, 41	prodrbdc 11375	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → (seq𝑚( · , 𝐹) ⇝ 𝑥 ↔ seq𝑤( · , 𝐹) ⇝ 𝑥))
43	22, 42	mpbid 146	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑤( · , 𝐹) ⇝ 𝑥)
44		simprr3 1032	. . . . . . . . . . . 12 ⊢ (((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧))) → seq𝑤( · , 𝐹) ⇝ 𝑧)
45	44	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑚 ∈ ℤ ∧ 𝑤 ∈ ℤ) ∧ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ_≥‘𝑤) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑤)DECID 𝑗 ∈ 𝐴 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧)))) → seq𝑤( · , 𝐹) ⇝ 𝑧)
46		climuni 11094	. . . . . . . . . . 11 ⊢ ((seq𝑤( · , 𝐹) ⇝ 𝑥 ∧ seq𝑤( · , 𝐹) ⇝ 𝑧) → 𝑥 = 𝑧)
47	43, 45, 46	syl2anc 409	. . . . . . . . . 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 2558	. . . . . . 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 11378	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) → 𝑧 = 𝑥))
55		equcomi 1681	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → 𝑥 = 𝑧)
56	54, 55	syl6 33	. . . . . . . 8 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧))
57	56	expimpd 361	. . . . . . 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 11378	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧))
61	60	expimpd 361	. . . . . 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 2603	. . . . . . . 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 1883	. . . . . . . . 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 2447	. . . . . . . 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 5790	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑤 → (1...𝑚) = (1...𝑤))
67	66	f1oeq2d 5371	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑤 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑤)–1-1-onto→𝐴))
68		fveq2 5429	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑤 → (seq1( · , 𝐺)‘𝑚) = (seq1( · , 𝐺)‘𝑤))
69	68	eqeq2d 2152	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑤 → (𝑧 = (seq1( · , 𝐺)‘𝑚) ↔ 𝑧 = (seq1( · , 𝐺)‘𝑤)))
70	67, 69	anbi12d 465	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑤 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤))))
71	70	exbidv 1798	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤))))
72		f1oeq1 5364	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓:(1...𝑤)–1-1-onto→𝐴 ↔ 𝑔:(1...𝑤)–1-1-onto→𝐴))
73		fveq1 5428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑗) = (𝑔‘𝑗))
74	73	csbeq1d 3014	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑔 → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑗) / 𝑘⦌𝐵)
75	74	ifeq1d 3494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑔 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1))
76	75	mpteq2dv 4027	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))
77	53, 76	syl5eq 2185	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))
78	77	seqeq3d 10257	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → seq1( · , 𝐺) = seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1))))
79	78	fveq1d 5431	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (seq1( · , 𝐺)‘𝑤) = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))
80	79	eqeq2d 2152	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑧 = (seq1( · , 𝐺)‘𝑤) ↔ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
81	72, 80	anbi12d 465	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝑓:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑤)) ↔ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))))
82	81	cbvexvw 1893	. . . . . . . . . . 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 2662	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑤 ∈ ℕ ∃𝑔(𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤)))
85	84	anbi2i 453	. . . . . . . 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 576	. . . . . . . . . 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 506	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
89		breq1 3940	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑎 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑎 ≤ (♯‘𝐴)))
90		fveq2 5429	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑎 → (𝑓‘𝑗) = (𝑓‘𝑎))
91	90	csbeq1d 3014	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑎 → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑎) / 𝑘⦌𝐵)
92	89, 91	ifbieq1d 3499	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑎 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 1))
93	92	cbvmptv 4032	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 1))
94	53, 93	eqtri 2161	. . . . . . . . . . . . 13 ⊢ 𝐺 = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑓‘𝑎) / 𝑘⦌𝐵, 1))
95		fveq2 5429	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑎 → (𝑔‘𝑗) = (𝑔‘𝑎))
96	95	csbeq1d 3014	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑎 → ⦋(𝑔‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑎) / 𝑘⦌𝐵)
97	89, 96	ifbieq1d 3499	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑎 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 1))
98	97	cbvmptv 4032	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)) = (𝑎 ∈ ℕ ↦ if(𝑎 ≤ (♯‘𝐴), ⦋(𝑔‘𝑎) / 𝑘⦌𝐵, 1))
99		simplr 520	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ))
100		simprl 521	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
101		simprr 522	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → 𝑔:(1...𝑤)–1-1-onto→𝐴)
102	23, 88, 94, 98, 99, 100, 101	prodmodclem3 11376	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑤)–1-1-onto→𝐴)) → (seq1( · , 𝐺)‘𝑚) = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))
103		eqeq12 2153	. . . . . . . . . . . 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 361	. . . . . . . . . 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 1870	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑤)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑘⦌𝐵, 1)))‘𝑤))) → 𝑥 = 𝑧))
108	107	rexlimdvva 2560	. . . . . . 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 949	. . . 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 1848	. 2 ⊢ (𝜑 → ∀𝑥∀𝑧(((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)))) → 𝑥 = 𝑧))
114		breq2 3941	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (seq𝑚( · , 𝐹) ⇝ 𝑥 ↔ seq𝑚( · , 𝐹) ⇝ 𝑧))
115	114	anbi2d 460	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)))
116	115	anbi2d 460	. . . . 5 ⊢ (𝑥 = 𝑧 → (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))))
117	116	rexbidv 2439	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧))))
118		eqeq1 2147	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 = (seq1( · , 𝐺)‘𝑚) ↔ 𝑧 = (seq1( · , 𝐺)‘𝑚)))
119	118	anbi2d 460	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
120	119	exbidv 1798	. . . . 5 ⊢ (𝑥 = 𝑧 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
121	120	rexbidv 2439	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚))))
122	117, 121	orbi12d 783	. . 3 ⊢ (𝑥 = 𝑧 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑧)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)))))
123	122	mo4 2061	. 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( · , 𝐺)‘𝑚))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ∨ wo 698 DECID wdc 820 ∧ w3a 963 ∀wal 1330 = wceq 1332 ∃wex 1469 ∈ wcel 1481 ∃*wmo 2001 ∀wral 2417 ∃wrex 2418 ⦋csb 3007 ⊆ wss 3076 ifcif 3479 class class class wbr 3937 ↦ cmpt 3997 –1-1-onto→wf1o 5130 ‘cfv 5131 (class class class)co 5782 ℂcc 7642 0cc0 7644 1c1 7645 · cmul 7649 ≤ cle 7825 # cap 8367 ℕcn 8744 ℤcz 9078 ℤ_≥cuz 9350 ...cfz 9821 seqcseq 10249 ♯chash 10553 ⇝ cli 11079

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 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-coll 4051 ax-sep 4054 ax-nul 4062 ax-pow 4106 ax-pr 4139 ax-un 4363 ax-setind 4460 ax-iinf 4510 ax-cnex 7735 ax-resscn 7736 ax-1cn 7737 ax-1re 7738 ax-icn 7739 ax-addcl 7740 ax-addrcl 7741 ax-mulcl 7742 ax-mulrcl 7743 ax-addcom 7744 ax-mulcom 7745 ax-addass 7746 ax-mulass 7747 ax-distr 7748 ax-i2m1 7749 ax-0lt1 7750 ax-1rid 7751 ax-0id 7752 ax-rnegex 7753 ax-precex 7754 ax-cnre 7755 ax-pre-ltirr 7756 ax-pre-ltwlin 7757 ax-pre-lttrn 7758 ax-pre-apti 7759 ax-pre-ltadd 7760 ax-pre-mulgt0 7761 ax-pre-mulext 7762 ax-arch 7763 ax-caucvg 7764

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-nel 2405 df-ral 2422 df-rex 2423 df-reu 2424 df-rmo 2425 df-rab 2426 df-v 2691 df-sbc 2914 df-csb 3008 df-dif 3078 df-un 3080 df-in 3082 df-ss 3089 df-nul 3369 df-if 3480 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-int 3780 df-iun 3823 df-br 3938 df-opab 3998 df-mpt 3999 df-tr 4035 df-id 4223 df-po 4226 df-iso 4227 df-iord 4296 df-on 4298 df-ilim 4299 df-suc 4301 df-iom 4513 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-rn 4558 df-res 4559 df-ima 4560 df-iota 5096 df-fun 5133 df-fn 5134 df-f 5135 df-f1 5136 df-fo 5137 df-f1o 5138 df-fv 5139 df-isom 5140 df-riota 5738 df-ov 5785 df-oprab 5786 df-mpo 5787 df-1st 6046 df-2nd 6047 df-recs 6210 df-irdg 6275 df-frec 6296 df-1o 6321 df-oadd 6325 df-er 6437 df-en 6643 df-dom 6644 df-fin 6645 df-pnf 7826 df-mnf 7827 df-xr 7828 df-ltxr 7829 df-le 7830 df-sub 7959 df-neg 7960 df-reap 8361 df-ap 8368 df-div 8457 df-inn 8745 df-2 8803 df-3 8804 df-4 8805 df-n0 9002 df-z 9079 df-uz 9351 df-q 9439 df-rp 9471 df-fz 9822 df-fzo 9951 df-seqfrec 10250 df-exp 10324 df-ihash 10554 df-cj 10646 df-re 10647 df-im 10648 df-rsqrt 10802 df-abs 10803 df-clim 11080

This theorem is referenced by: fprodseq 11384

W3C validator