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	$⊢ A = B$
	cbvprodvw2.2	$⊢ j = k \to C = D$
Assertion	cbvprodvw2	$⊢ \prod_{j \in A} C = \prod_{k \in B} D$

Proof

Step	Hyp	Ref	Expression
1		cbvprodvw2.1	$⊢ A = B$
2		cbvprodvw2.2	$⊢ j = k \to C = D$
3	1	sseq1i	$⊢ A \subseteq ℤ_{\geq m} \leftrightarrow B \subseteq ℤ_{\geq m}$
4	1	eleq2i	$⊢ j \in A \leftrightarrow j \in B$
5		eleq1w	$⊢ j = k \to (j \in B \leftrightarrow k \in B)$
6	4 5	bitrid	$⊢ j = k \to (j \in A \leftrightarrow k \in B)$
7	6 2	ifbieq1d	$⊢ j = k \to if (j \in A, C, 1) = if (k \in B, D, 1)$
8	7	cbvmptv	$⊢ (j \in ℤ ⟼ if (j \in A, C, 1)) = (k \in ℤ ⟼ if (k \in B, D, 1))$
9		seqeq3	$⊢ (j \in ℤ ⟼ if (j \in A, C, 1)) = (k \in ℤ ⟼ if (k \in B, D, 1)) \to seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1)))$
10	8 9	ax-mp	$⊢ seq n (\times (j \in ℤ ⟼ if (j \in A, C, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in B, D, 1)))$
11	10	breq1i	$⊢ 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$
12	11	anbi2i	$⊢ (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)$
13	12	exbii	$⊢ \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)$
14	13	rexbii	$⊢ \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)$
15		seqeq3	$⊢ (j \in ℤ ⟼ if (j \in A, C, 1)) = (k \in ℤ ⟼ if (k \in B, D, 1)) \to seq m (\times (j \in ℤ ⟼ if (j \in A, C, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in B, D, 1)))$
16	8 15	ax-mp	$⊢ seq m (\times (j \in ℤ ⟼ if (j \in A, C, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in B, D, 1)))$
17	16	breq1i	$⊢ 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$
18	3 14 17	3anbi123i	$⊢ (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)$
19	18	rexbii	$⊢ \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)$
20		f1oeq3	$⊢ A = B \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots m) \underset{1-1 onto}{⟶} B)$
21	1 20	ax-mp	$⊢ f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots m) \underset{1-1 onto}{⟶} B$
22	2	cbvcsbv	$⊢ ⦋ f (n) / j ⦌ C = ⦋ f (n) / k ⦌ D$
23	22	mpteq2i	$⊢ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)$
24		seqeq3	$⊢ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D) \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D))$
25	23 24	ax-mp	$⊢ seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D))$
26	25	fveq1i	$⊢ seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)$
27	26	eqeq2i	$⊢ x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ C)) (m) \leftrightarrow x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ D)) (m)$
28	21 27	anbi12i	$⊢ (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))$
29	28	exbii	$⊢ \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))$
30	29	rexbii	$⊢ \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))$
31	19 30	orbi12i	$⊢ (\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)))$
32	31	iotabii	$⊢ (ι 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))))$
33		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))))$
34		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))))$
35	32 33 34	3eqtr4i	$⊢ \prod_{j \in A} C = \prod_{k \in B} D$

Metamath Proof Explorer

Theorem cbvprodvw2

Proof