Theorem cbvprodvw2 37251

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 3941	. . . . . 6 ⊢ (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐵 ⊆ (ℤ≥‘𝑚))
3	1	eleq2i 2856	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ 𝐴 ↔ 𝑗 ∈ 𝐵)
4		eleq1w 2847	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐵 ↔ 𝑘 ∈ 𝐵))
5	3, 4	bitrid 286	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐵))
6		cbvprodvw2.2	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)
7	5, 6	ifbieq1d 4510	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → if(𝑗 ∈ 𝐴, 𝐶, 1) = if(𝑘 ∈ 𝐵, 𝐷, 1))
8	7	cbvmptv 5215	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))
9		seqeq3 14189	. . . . . . . . . . 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 5115	. . . . . . . . 9 ⊢ (seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦)
12	11	anbi2i 635	. . . . . . . 8 ⊢ ((𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦))
13	12	exbii 1881	. . . . . . 7 ⊢ (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦))
14	13	rexbii 3113	. . . . . 6 ⊢ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦))
15		seqeq3 14189	. . . . . . . 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 5115	. . . . . 6 ⊢ (seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥)
18	2, 14, 17	3anbi123i 1173	. . . . 5 ⊢ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥))
19	18	rexbii 3113	. . . 4 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥))
20		f1oeq3 6844	. . . . . . . 8 ⊢ (𝐴 = 𝐵 → (𝑓:(1...𝑚)⟶1-1onto𝐴 ↔ 𝑓:(1...𝑚)⟶1-1onto𝐵))
21	1, 20	ax-mp 5	. . . . . . 7 ⊢ (𝑓:(1...𝑚)⟶1-1onto𝐴 ↔ 𝑓:(1...𝑚)⟶1-1onto𝐵)
22	6	cbvcsbv 3863	. . . . . . . . . . 11 ⊢ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐷
23	22	mpteq2i 5207	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷)
24		seqeq3 14189	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷) → seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶)) = seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷)))
25	23, 24	ax-mp 5	. . . . . . . . 9 ⊢ seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶)) = seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))
26	25	fveq1i 6917	. . . . . . . 8 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚)
27	26	eqeq2i 2776	. . . . . . 7 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚))
28	21, 27	anbi12i 640	. . . . . 6 ⊢ ((𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚)) ↔ (𝑓:(1...𝑚)⟶1-1onto𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚)))
29	28	exbii 1881	. . . . 5 ⊢ (∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚)))
30	29	rexbii 3113	. . . 4 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚)))
31	19, 30	orbi12i 928	. . 3 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚))))
32	31	iotabii 6550	. 2 ⊢ (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚))))
33		df-prod 16117	. 2 ⊢ ∏𝑗 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑗⦌𝐶))‘𝑚))))
34		df-prod 16117	. 2 ⊢ ∏𝑘 ∈ 𝐵 𝐷 = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐷))‘𝑚))))
35	32, 33, 34	3eqtr4i 2796	1 ⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ≠ wne 2959  ∃wrex 3090  ⦋csb 3851   ⊆ wss 3900  ifcif 4485   class class class wbr 5108   ↦ cmpt 5192  ℩cio 6518  ⟶1-1ontowf1o 6565  ‘cfv 6566  (class class class)co 7451  0cc0 11239  1c1 11240   · cmul 11244  ℕcn 12375  ℤcz 12733  ℤ_≥cuz 13005  ...cfz 13679  seqcseq 14184   ⇝ cli 15695  ∏cprod 16116

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-xp 5664  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-iota 6520  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-seq 14185  df-prod 16117

This theorem is used by: (None)