Metamath Proof Explorer

Theorem 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 ⊢ Ⅎ _ x A
nfcprod.2 ⊢ Ⅎ _ x B
Assertion nfcprod ⊢ Ⅎ _ x ∏ k ∈ A B

Proof

Step Hyp Ref Expression
1 nfcprod.1 ⊢ Ⅎ _ x A
2 nfcprod.2 ⊢ Ⅎ _ x B
3 df-prod ⊢ ∏ k ∈ A B = ι y | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ z z ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ z ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ y = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
4 nfcv ⊢ Ⅎ _ x ℤ
5 nfcv ⊢ Ⅎ _ x ℤ ≥ m
6 1 5 nfss ⊢ Ⅎ x A ⊆ ℤ ≥ m
7 nfv ⊢ Ⅎ x z ≠ 0
8 nfcv ⊢ Ⅎ _ x n
9 nfcv ⊢ Ⅎ _ x ×
10 1 nfcri ⊢ Ⅎ x k ∈ A
11 nfcv ⊢ Ⅎ _ x 1
12 10 2 11 nfif ⊢ Ⅎ _ x if k ∈ A B 1
13 4 12 nfmpt ⊢ Ⅎ _ x k ∈ ℤ ⟼ if k ∈ A B 1
14 8 9 13 nfseq ⊢ Ⅎ _ x seq n × k ∈ ℤ ⟼ if k ∈ A B 1
15 nfcv ⊢ Ⅎ _ x ⇝
16 nfcv ⊢ Ⅎ _ x z
17 14 15 16 nfbr ⊢ Ⅎ x seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ z
18 7 17 nfan ⊢ Ⅎ x z ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ z
19 18 nfex ⊢ Ⅎ x ∃ z z ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ z
20 5 19 nfrexw ⊢ Ⅎ x ∃ n ∈ ℤ ≥ m ∃ z z ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ z
21 nfcv ⊢ Ⅎ _ x m
22 21 9 13 nfseq ⊢ Ⅎ _ x seq m × k ∈ ℤ ⟼ if k ∈ A B 1
23 nfcv ⊢ Ⅎ _ x y
24 22 15 23 nfbr ⊢ Ⅎ x seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y
25 6 20 24 nf3an ⊢ Ⅎ x A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ z z ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ z ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y
26 4 25 nfrexw ⊢ Ⅎ x ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ z z ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ z ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y
27 nfcv ⊢ Ⅎ _ x ℕ
28 nfcv ⊢ Ⅎ _ x f
29 nfcv ⊢ Ⅎ _ x 1 … m
30 28 29 1 nff1o ⊢ Ⅎ x f : 1 … m ⟶ 1-1 onto A
31 nfcv ⊢ Ⅎ _ x f ⁡ n
32 31 2 nfcsbw ⊢ Ⅎ _ x ⦋ f ⁡ n / k⦌ B
33 27 32 nfmpt ⊢ Ⅎ _ x n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B
34 11 9 33 nfseq ⊢ Ⅎ _ x seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B
35 34 21 nffv ⊢ Ⅎ _ x seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
36 35 nfeq2 ⊢ Ⅎ x y = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
37 30 36 nfan ⊢ Ⅎ x f : 1 … m ⟶ 1-1 onto A ∧ y = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
38 37 nfex ⊢ Ⅎ x ∃ f f : 1 … m ⟶ 1-1 onto A ∧ y = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
39 27 38 nfrexw ⊢ Ⅎ x ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ y = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
40 26 39 nfor ⊢ Ⅎ x ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ z z ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ z ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ y = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
41 40 nfiotaw ⊢ Ⅎ _ x ι y | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ z z ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ z ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ y = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
42 3 41 nfcxfr ⊢ Ⅎ _ x ∏ k ∈ A B