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
|- 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 )