Metamath Proof Explorer

Theorem cbvprodvw2

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

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

Proof

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