# Metamath Proof Explorer

## Theorem nfcprod1

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

Ref Expression
Hypothesis nfcprod1.1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
Assertion nfcprod1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\prod _{{k}\in {A}}{B}$

### Proof

Step Hyp Ref Expression
1 nfcprod1.1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
2 df-prod
3 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}ℤ$
4 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{ℤ}_{\ge {m}}$
5 1 4 nfss ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{A}\subseteq {ℤ}_{\ge {m}}$
6 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{y}\ne 0$
7 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{n}$
8 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}×$
9 nfmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
10 7 8 9 nfseq ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)$
11 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}⇝$
12 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{y}$
13 10 11 12 nfbr ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}$
14 6 13 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}\right)$
15 14 nfex ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}\right)$
16 4 15 nfrex ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}\right)$
17 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{m}$
18 17 8 9 nfseq ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)$
19 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{x}$
20 18 11 19 nfbr ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{x}$
21 5 16 20 nf3an ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{x}\right)$
22 3 21 nfrex ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{x}\right)$
23 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}ℕ$
24 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{f}$
25 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left(1\dots {m}\right)$
26 24 25 1 nff1o ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}$
27 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}1$
28 nfcsb1v
29 23 28 nfmpt
30 27 8 29 nfseq
31 30 17 nffv
32 31 nfeq2
33 26 32 nfan
34 33 nfex
35 23 34 nfrex
36 22 35 nfor
37 36 nfiotaw
38 2 37 nfcxfr ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\prod _{{k}\in {A}}{B}$