# Metamath Proof Explorer

## Theorem fprodcllemf

Description: Finite product closure lemma. A version of fprodcllem using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodcllemf.ph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
fprodcllemf.s ${⊢}{\phi }\to {S}\subseteq ℂ$
fprodcllemf.xy ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
fprodcllemf.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fprodcllemf.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {S}$
fprodcllemf.1 ${⊢}{\phi }\to 1\in {S}$
Assertion fprodcllemf ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}\in {S}$

### Proof

Step Hyp Ref Expression
1 fprodcllemf.ph ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 fprodcllemf.s ${⊢}{\phi }\to {S}\subseteq ℂ$
3 fprodcllemf.xy ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
4 fprodcllemf.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
5 fprodcllemf.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {S}$
6 fprodcllemf.1 ${⊢}{\phi }\to 1\in {S}$
7 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{B}$
8 nfcsb1v
9 csbeq1a
10 7 8 9 cbvprodi
11 5 ex ${⊢}{\phi }\to \left({k}\in {A}\to {B}\in {S}\right)$
12 1 11 ralrimi ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {S}$
13 rspsbc
14 12 13 mpan9
15 sbcel1g
16 15 elv
17 14 16 sylib
18 2 3 4 17 6 fprodcllem
19 10 18 eqeltrid ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}\in {S}$