This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )