Theorem cbvprod 15946

Description: Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)

Hypotheses

Ref	Expression
cbvprod.1	⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
cbvprod.2	⊢ Ⅎ𝑘𝐴
cbvprod.3	⊢ Ⅎ𝑗𝐴
cbvprod.4	⊢ Ⅎ𝑘𝐵
cbvprod.5	⊢ Ⅎ𝑗𝐶

Assertion

Ref	Expression
cbvprod	⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶

Distinct variable group:   𝑗,𝑘

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

Proof of Theorem cbvprod

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

Step	Hyp	Ref	Expression
1		biid 261	. . . . . 6 ⊢ (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐴 ⊆ (ℤ≥‘𝑚))
2		cbvprod.2	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘𝐴
3	2	nfcri 2895	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑗 ∈ 𝐴
4		cbvprod.4	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘𝐵
5		nfcv 2903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘1
6	3, 4, 5	nfif 4561	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘if(𝑗 ∈ 𝐴, 𝐵, 1)
7		cbvprod.3	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝐴
8	7	nfcri 2895	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑘 ∈ 𝐴
9		cbvprod.5	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝐶
10		nfcv 2903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗1
11	8, 9, 10	nfif 4561	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗if(𝑘 ∈ 𝐴, 𝐶, 1)
12		eleq1w 2822	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
13		cbvprod.1	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)
14	12, 13	ifbieq1d 4555	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → if(𝑗 ∈ 𝐴, 𝐵, 1) = if(𝑘 ∈ 𝐴, 𝐶, 1))
15	6, 11, 14	cbvmpt 5259	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))
16		seqeq3 14044	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)) → seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))))
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)))
18	17	breq1i 5155	. . . . . . . . 9 ⊢ (seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)
19	18	anbi2i 623	. . . . . . . 8 ⊢ ((𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦))
20	19	exbii 1845	. . . . . . 7 ⊢ (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦))
21	20	rexbii 3092	. . . . . 6 ⊢ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦))
22		seqeq3 14044	. . . . . . . 8 ⊢ ((𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)) → seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))))
23	15, 22	ax-mp 5	. . . . . . 7 ⊢ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)))
24	23	breq1i 5155	. . . . . 6 ⊢ (seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥)
25	1, 21, 24	3anbi123i 1154	. . . . 5 ⊢ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥))
26	25	rexbii 3092	. . . 4 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥))
27	4, 9, 13	cbvcsbw 3918	. . . . . . . . . . 11 ⊢ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶
28	27	mpteq2i 5253	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)
29		seqeq3 14044	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶) → seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵)) = seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)))
30	28, 29	ax-mp 5	. . . . . . . . 9 ⊢ seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵)) = seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))
31	30	fveq1i 6908	. . . . . . . 8 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)
32	31	eqeq2i 2748	. . . . . . 7 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))
33	32	anbi2i 623	. . . . . 6 ⊢ ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
34	33	exbii 1845	. . . . 5 ⊢ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
35	34	rexbii 3092	. . . 4 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
36	26, 35	orbi12i 914	. . 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( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
37	36	iotabii 6548	. 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( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
38		df-prod 15937	. 2 ⊢ ∏𝑗 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐵))‘𝑚))))
39		df-prod 15937	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
40	37, 38, 39	3eqtr4i 2773	1 ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1537  ∃wex 1776   ∈ wcel 2106  Ⅎwnfc 2888   ≠ wne 2938  ∃wrex 3068  ⦋csb 3908   ⊆ wss 3963  ifcif 4531   class class class wbr 5148   ↦ cmpt 5231  ℩cio 6514  –1-1-onto→wf1o 6562  ‘cfv 6563  (class class class)co 7431  0cc0 11153  1c1 11154   · cmul 11158  ℕcn 12264  ℤcz 12611  ℤ_≥cuz 12876  ...cfz 13544  seqcseq 14039   ⇝ cli 15517  ∏cprod 15936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5695  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-iota 6516  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-seq 14040  df-prod 15937

This theorem is referenced by:  cbvprodi  15948  vonn0ioo2  46646  vonn0icc2  46648