Theorem cbvprodvw2 36190

Description: Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025.)

Hypotheses

Ref	Expression
cbvprodvw2.1	⊢ 𝐴 = 𝐵
cbvprodvw2.2	⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)

Assertion

Ref	Expression
cbvprodvw2	⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷

Distinct variable groups:   𝑗,𝑘   𝐷,𝑗   𝐶,𝑘   𝐴,𝑘   𝐵,𝑗

Allowed substitution hints:   𝐴(𝑗)   𝐵(𝑘)   𝐶(𝑗)   𝐷(𝑘)

Proof of Theorem cbvprodvw2

Dummy variables 𝑥 𝑦 𝑚 𝑛 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cbvprodvw2.1	. . . . . . 7 ⊢ 𝐴 = 𝐵
2	1	sseq1i 4024	. . . . . 6 ⊢ (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐵 ⊆ (ℤ≥‘𝑚))
3	1	eleq2i 2829	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ 𝐴 ↔ 𝑗 ∈ 𝐵)
4		eleq1w 2820	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐵 ↔ 𝑘 ∈ 𝐵))
5	3, 4	bitrid 283	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐵))
6		cbvprodvw2.2	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)
7	5, 6	ifbieq1d 4554	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → if(𝑗 ∈ 𝐴, 𝐶, 1) = if(𝑘 ∈ 𝐵, 𝐷, 1))
8	7	cbvmptv 5262	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))
9		seqeq3 14033	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1)) → seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))))
10	8, 9	ax-mp 5	. . . . . . . . . 10 ⊢ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1)))
11	10	breq1i 5156	. . . . . . . . 9 ⊢ (seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦)
12	11	anbi2i 622	. . . . . . . 8 ⊢ ((𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦))
13	12	exbii 1843	. . . . . . 7 ⊢ (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦))
14	13	rexbii 3090	. . . . . 6 ⊢ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦))
15		seqeq3 14033	. . . . . . . 8 ⊢ ((𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1)) → seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))))
16	8, 15	ax-mp 5	. . . . . . 7 ⊢ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1)))
17	16	breq1i 5156	. . . . . 6 ⊢ (seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥)
18	2, 14, 17	3anbi123i 1153	. . . . 5 ⊢ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥))
19	18	rexbii 3090	. . . 4 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥))
20		f1oeq3 6833	. . . . . . . 8 ⊢ (𝐴 = 𝐵 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑚)–1-1-onto→𝐵))
21	1, 20	ax-mp 5	. . . . . . 7 ⊢ (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑚)–1-1-onto→𝐵)
22	6	cbvcsbv 3920	. . . . . . . . . . 11 ⊢ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐷
23	22	mpteq2i 5254	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷)
24		seqeq3 14033	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷) → seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶)) = seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷)))
25	23, 24	ax-mp 5	. . . . . . . . 9 ⊢ seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶)) = seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))
26	25	fveq1i 6902	. . . . . . . 8 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚)
27	26	eqeq2i 2746	. . . . . . 7 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚))
28	21, 27	anbi12i 627	. . . . . 6 ⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚)))
29	28	exbii 1843	. . . . 5 ⊢ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚)))
30	29	rexbii 3090	. . . 4 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚)))
31	19, 30	orbi12i 913	. . 3 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚))))
32	31	iotabii 6543	. 2 ⊢ (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚))))
33		df-prod 15926	. 2 ⊢ ∏𝑗 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚))))
34		df-prod 15926	. 2 ⊢ ∏𝑘 ∈ 𝐵 𝐷 = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚))))
35	32, 33, 34	3eqtr4i 2771	1 ⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∧ w3a 1085   = wceq 1535  ∃wex 1774   ∈ wcel 2104   ≠ wne 2936  ∃wrex 3066  ⦋csb 3908   ⊆ wss 3963  ifcif 4530   class class class wbr 5149   ↦ cmpt 5232  ℩cio 6508  –1-1-onto→wf1o 6557  ‘cfv 6558  (class class class)co 7425  0cc0 11146  1c1 11147   · cmul 11151  ℕcn 12257  ℤcz 12604  ℤ_≥cuz 12869  ...cfz 13537  seqcseq 14028   ⇝ cli 15506  ∏cprod 15925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-ext 2704

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-sb 2061  df-clab 2711  df-cleq 2725  df-clel 2812  df-ral 3058  df-rex 3067  df-rab 3433  df-v 3479  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4915  df-br 5150  df-opab 5212  df-mpt 5233  df-xp 5689  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6317  df-iota 6510  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7428  df-oprab 7429  df-mpo 7430  df-frecs 8299  df-wrecs 8330  df-recs 8404  df-rdg 8443  df-seq 14029  df-prod 15926

This theorem is referenced by: (None)