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\phi$$
	fprodcllemf.s	$$⊢\phi \to S\subseteq ℂ$$
	fprodcllemf.xy	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xy\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\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 xy\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{\_}{Ⅎ}jB$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋j/k⦌B$$
9		csbeq1a	$$⊢k=j\to B=⦋j/k⦌B$$
10	7 8 9	cbvprodi	$$⊢\prod _{k\in A}B=\prod _{j\in A}⦋j/k⦌B$$
11	5	ex	$$⊢\phi \to \left(k\in A\to B\in S\right)$$
12	1 11	ralrimi	$$⊢\phi \to \forall k\in AB\in S$$
13		rspsbc	$$⊢j\in A\to \left(\forall k\in AB\in S\to \underset{\dot{}}{[}j/k\underset{\dot{}}{]}B\in S\right)$$
14	12 13	mpan9	$$⊢\left(\phi \wedge j\in A\right)\to \underset{\dot{}}{[}j/k\underset{\dot{}}{]}B\in S$$
15		sbcel1g	$$⊢j\in \mathrm{V}\to \left(\underset{\dot{}}{[}j/k\underset{\dot{}}{]}B\in S\leftrightarrow ⦋j/k⦌B\in S\right)$$
16	15	elv	$$⊢\underset{\dot{}}{[}j/k\underset{\dot{}}{]}B\in S\leftrightarrow ⦋j/k⦌B\in S$$
17	14 16	sylib	$$⊢\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in S$$
18	2 3 4 17 6	fprodcllem	$$⊢\phi \to \prod _{j\in A}⦋j/k⦌B\in S$$
19	10 18	eqeltrid	$$⊢\phi \to \prod _{k\in A}B\in S$$