nfcprod1

Description: Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017)

		Ref	Expression
	Hypothesis	nfcprod1.1	$⊢ \underline{Ⅎ} k A$
	Assertion	nfcprod1	$⊢ \underline{Ⅎ} k \prod_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		nfcprod1.1	$⊢ \underline{Ⅎ} k A$
2		df-prod	$⊢ \prod_{k \in A} B = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 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) / k ⦌ B)) (m))))$
3		nfcv	$⊢ \underline{Ⅎ} k ℤ$
4		nfcv	$⊢ \underline{Ⅎ} k ℤ_{\geq m}$
5	1 4	nfss	$⊢ Ⅎ k A \subseteq ℤ_{\geq m}$
6		nfv	$⊢ Ⅎ k y \neq 0$
7		nfcv	$⊢ \underline{Ⅎ} k n$
8		nfcv	$⊢ \underline{Ⅎ} k \times$
9		nfmpt1	$⊢ \underline{Ⅎ} k (k \in ℤ ⟼ if (k \in A, B, 1))$
10	7 8 9	nfseq	$⊢ \underline{Ⅎ} k seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1)))$
11		nfcv	$⊢ \underline{Ⅎ} k ⇝$
12		nfcv	$⊢ \underline{Ⅎ} k y$
13	10 11 12	nfbr	$⊢ Ⅎ k seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y$
14	6 13	nfan	$⊢ Ⅎ k (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y)$
15	14	nfex	$⊢ Ⅎ k \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y)$
16	4 15	nfrex	$⊢ Ⅎ k \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y)$
17		nfcv	$⊢ \underline{Ⅎ} k m$
18	17 8 9	nfseq	$⊢ \underline{Ⅎ} k seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1)))$
19		nfcv	$⊢ \underline{Ⅎ} k x$
20	18 11 19	nfbr	$⊢ Ⅎ k seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x$
21	5 16 20	nf3an	$⊢ Ⅎ k (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
22	3 21	nfrex	$⊢ Ⅎ k \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
23		nfcv	$⊢ \underline{Ⅎ} k ℕ$
24		nfcv	$⊢ \underline{Ⅎ} k f$
25		nfcv	$⊢ \underline{Ⅎ} k (1 \dots m)$
26	24 25 1	nff1o	$⊢ Ⅎ k f : (1 \dots m) \underset{1-1 onto}{⟶} A$
27		nfcv	$⊢ \underline{Ⅎ} k 1$
28		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ f (n) / k ⦌ B$
29	23 28	nfmpt	$⊢ \underline{Ⅎ} k (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)$
30	27 8 29	nfseq	$⊢ \underline{Ⅎ} k seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B))$
31	30 17	nffv	$⊢ \underline{Ⅎ} k seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
32	31	nfeq2	$⊢ Ⅎ k x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
33	26 32	nfan	$⊢ Ⅎ k (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
34	33	nfex	$⊢ Ⅎ k \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
35	23 34	nfrex	$⊢ Ⅎ k \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
36	22 35	nfor	$⊢ Ⅎ k (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 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) / k ⦌ B)) (m)))$
37	36	nfiotaw	$⊢ \underline{Ⅎ} k (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 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) / k ⦌ B)) (m))))$
38	2 37	nfcxfr	$⊢ \underline{Ⅎ} k \prod_{k \in A} B$

Metamath Proof Explorer

Theorem nfcprod1

Proof