Theorem fprodcllem

Description: Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017)

	Ref	Expression
Hypotheses	fprodcllem.1	$$⊢\phi \to S\subseteq ℂ$$
	fprodcllem.2	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xy\in S$$
	fprodcllem.3	$$⊢\phi \to A\in \mathrm{Fin}$$
	fprodcllem.4	$$⊢\left(\phi \wedge k\in A\right)\to B\in S$$
	fprodcllem.5	$$⊢\phi \to 1\in S$$
Assertion	fprodcllem	$$⊢\phi \to \prod _{k\in A}B\in S$$

Proof

Step	Hyp	Ref	Expression
1		fprodcllem.1	$$⊢\phi \to S\subseteq ℂ$$
2		fprodcllem.2	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xy\in S$$
3		fprodcllem.3	$$⊢\phi \to A\in \mathrm{Fin}$$
4		fprodcllem.4	$$⊢\left(\phi \wedge k\in A\right)\to B\in S$$
5		fprodcllem.5	$$⊢\phi \to 1\in S$$
6		prodeq1	$$⊢A=\varnothing \to \prod _{k\in A}B=\prod _{k\in \varnothing }B$$
7		prod0	$$⊢\prod _{k\in \varnothing }B=1$$
8	6 7	eqtrdi	$$⊢A=\varnothing \to \prod _{k\in A}B=1$$
9	8	adantl	$$⊢\left(\phi \wedge A=\varnothing \right)\to \prod _{k\in A}B=1$$
10	5	adantr	$$⊢\left(\phi \wedge A=\varnothing \right)\to 1\in S$$
11	9 10	eqeltrd	$$⊢\left(\phi \wedge A=\varnothing \right)\to \prod _{k\in A}B\in S$$
12	1	adantr	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to S\subseteq ℂ$$
13	2	adantlr	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \left(x\in S\wedge y\in S\right)\right)\to xy\in S$$
14	3	adantr	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to A\in \mathrm{Fin}$$
15	4	adantlr	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge k\in A\right)\to B\in S$$
16		simpr	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to A\ne \varnothing$$
17	12 13 14 15 16	fprodcl2lem	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to \prod _{k\in A}B\in S$$
18	11 17	pm2.61dane	$$⊢\phi \to \prod _{k\in A}B\in S$$