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	|- F/ k ph
	fprodcllemf.s	|- ( ph -> S C_ CC )
	fprodcllemf.xy	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
	fprodcllemf.a	|- ( ph -> A e. Fin )
	fprodcllemf.b	|- ( ( ph /\ k e. A ) -> B e. S )
	fprodcllemf.1	|- ( ph -> 1 e. S )
Assertion	fprodcllemf	|- ( ph -> prod_ k e. A B e. S )

Proof

Step	Hyp	Ref	Expression
1		fprodcllemf.ph	|- F/ k ph
2		fprodcllemf.s	|- ( ph -> S C_ CC )
3		fprodcllemf.xy	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
4		fprodcllemf.a	|- ( ph -> A e. Fin )
5		fprodcllemf.b	|- ( ( ph /\ k e. A ) -> B e. S )
6		fprodcllemf.1	|- ( ph -> 1 e. S )
7		nfcv	|- F/_ j B
8		nfcsb1v	|- F/_ k [_ j / k ]_ B
9		csbeq1a	|- ( k = j -> B = [_ j / k ]_ B )
10	7 8 9	cbvprodi	|- prod_ k e. A B = prod_ j e. A [_ j / k ]_ B
11	5	ex	|- ( ph -> ( k e. A -> B e. S ) )
12	1 11	ralrimi	|- ( ph -> A. k e. A B e. S )
13		rspsbc	|- ( j e. A -> ( A. k e. A B e. S -> [. j / k ]. B e. S ) )
14	12 13	mpan9	|- ( ( ph /\ j e. A ) -> [. j / k ]. B e. S )
15		sbcel1g	|- ( j e. _V -> ( [. j / k ]. B e. S <-> [_ j / k ]_ B e. S ) )
16	15	elv	|- ( [. j / k ]. B e. S <-> [_ j / k ]_ B e. S )
17	14 16	sylib	|- ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. S )
18	2 3 4 17 6	fprodcllem	|- ( ph -> prod_ j e. A [_ j / k ]_ B e. S )
19	10 18	eqeltrid	|- ( ph -> prod_ k e. A B e. S )