Theorem fprodcllem

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

	Ref	Expression
Hypotheses	fprodcllem.1	|- ( ph -> S C_ CC )
	fprodcllem.2	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
	fprodcllem.3	|- ( ph -> A e. Fin )
	fprodcllem.4	|- ( ( ph /\ k e. A ) -> B e. S )
	fprodcllem.5	|- ( ph -> 1 e. S )
Assertion	fprodcllem	|- ( ph -> prod_ k e. A B e. S )

Proof

Step	Hyp	Ref	Expression
1		fprodcllem.1	|- ( ph -> S C_ CC )
2		fprodcllem.2	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
3		fprodcllem.3	|- ( ph -> A e. Fin )
4		fprodcllem.4	|- ( ( ph /\ k e. A ) -> B e. S )
5		fprodcllem.5	|- ( ph -> 1 e. S )
6		prodeq1	|- ( A = (/) -> prod_ k e. A B = prod_ k e. (/) B )
7		prod0	|- prod_ k e. (/) B = 1
8	6 7	eqtrdi	|- ( A = (/) -> prod_ k e. A B = 1 )
9	8	adantl	|- ( ( ph /\ A = (/) ) -> prod_ k e. A B = 1 )
10	5	adantr	|- ( ( ph /\ A = (/) ) -> 1 e. S )
11	9 10	eqeltrd	|- ( ( ph /\ A = (/) ) -> prod_ k e. A B e. S )
12	1	adantr	|- ( ( ph /\ A =/= (/) ) -> S C_ CC )
13	2	adantlr	|- ( ( ( ph /\ A =/= (/) ) /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
14	3	adantr	|- ( ( ph /\ A =/= (/) ) -> A e. Fin )
15	4	adantlr	|- ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> B e. S )
16		simpr	|- ( ( ph /\ A =/= (/) ) -> A =/= (/) )
17	12 13 14 15 16	fprodcl2lem	|- ( ( ph /\ A =/= (/) ) -> prod_ k e. A B e. S )
18	11 17	pm2.61dane	|- ( ph -> prod_ k e. A B e. S )