cbvproddavw2

Description: Change bound variable and the set of integers in a product. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvproddavw2.1	$⊢ φ \to A = B$
	cbvproddavw2.2	$⊢ (φ \land j = k) \to C = D$
Assertion	cbvproddavw2	$⊢ φ \to \prod_{j \in A} C = \prod_{k \in B} D$

Proof

Step	Hyp	Ref	Expression
1		cbvproddavw2.1	$⊢ φ \to A = B$
2		cbvproddavw2.2	$⊢ (φ \land j = k) \to C = D$
3	1	sseq1d	$⊢ φ \to (A \subseteq ℤ_{\geq m} \leftrightarrow B \subseteq ℤ_{\geq m})$
4		simpr	$⊢ (φ \land j = k) \to j = k$
5	1	adantr	$⊢ (φ \land j = k) \to A = B$
6	4 5	eleq12d	$⊢ (φ \land j = k) \to (j \in A \leftrightarrow k \in B)$
7	6 2	ifbieq1d	$⊢ (φ \land j = k) \to if (j \in A, C, 1) = if (k \in B, D, 1)$
8	7	cbvmptdavw	$⊢ φ \to (j \in ℤ ⟼ if (j \in A, C, 1)) = (k \in ℤ ⟼ if (k \in B, D, 1))$
9	8	seqeq3d	$⊢ φ \to seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1)))$
10	9	breq1d	$⊢ φ \to (seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ y \leftrightarrow seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ y)$
11	10	anbi2d	$⊢ φ \to ((y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ y) \leftrightarrow (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ y))$
12	11	exbidv	$⊢ φ \to (\exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ y) \leftrightarrow \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ y))$
13	12	rexbidv	$⊢ φ \to (\exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ y) \leftrightarrow \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ y))$
14	8	seqeq3d	$⊢ φ \to seq m (\times (j \in ℤ ⟼ if (j \in A, C, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in B, D, 1)))$
15	14	breq1d	$⊢ φ \to (seq m (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ x \leftrightarrow seq m (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ x)$
16	3 13 15	3anbi123d	$⊢ φ \to ((A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ x) \leftrightarrow (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ x))$
17	16	rexbidv	$⊢ φ \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ x) \leftrightarrow \exists m \in ℤ (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ x))$
18	1	f1oeq3d	$⊢ φ \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots m) \underset{1-1 onto}{⟶} B)$
19	2	cbvcsbdavw	$⊢ φ \to ⦋ f (n) / j ⦌ C = ⦋ f (n) / k ⦌ D$
20	19	mpteq2dv	$⊢ φ \to (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)$
21	20	seqeq3d	$⊢ φ \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D))$
22	21	fveq1d	$⊢ φ \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)$
23	22	eqeq2d	$⊢ φ \to (x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m) \leftrightarrow x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m))$
24	18 23	anbi12d	$⊢ φ \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)))$
25	24	exbidv	$⊢ φ \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)))$
26	25	rexbidv	$⊢ φ \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m)) \leftrightarrow \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)))$
27	17 26	orbi12d	$⊢ φ \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m))) \leftrightarrow (\exists m \in ℤ (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m))))$
28	27	iotabidv	$⊢ φ \to (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m)))) = (ι x \| (\exists m \in ℤ (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m))))$
29		df-prod	$⊢ \prod_{j \in A} C = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, C, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m))))$
30		df-prod	$⊢ \prod_{k \in B} D = (ι x \| (\exists m \in ℤ (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, D, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m))))$
31	28 29 30	3eqtr4g	$⊢ φ \to \prod_{j \in A} C = \prod_{k \in B} D$

Metamath Proof Explorer

Theorem cbvproddavw2

Proof