nfcprod

Description: Bound-variable hypothesis builder for product: if x is (effectively) not free in A and B , it is not free in prod_ k e. A B . (Contributed by Scott Fenton, 1-Dec-2017)

	Ref	Expression
Hypotheses	nfcprod.1	$⊢ \underline{Ⅎ} x A$
	nfcprod.2	$⊢ \underline{Ⅎ} x B$
Assertion	nfcprod	$⊢ \underline{Ⅎ} x \prod_{k \in A} B$

Proof

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

Metamath Proof Explorer

Theorem nfcprod

Proof