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 kφ
fprodcllemf.s φS
fprodcllemf.xy φxSySxyS
fprodcllemf.a φAFin
fprodcllemf.b φkABS
fprodcllemf.1 φ1S
Assertion fprodcllemf φkABS

Proof

Step Hyp Ref Expression
1 fprodcllemf.ph kφ
2 fprodcllemf.s φS
3 fprodcllemf.xy φxSySxyS
4 fprodcllemf.a φAFin
5 fprodcllemf.b φkABS
6 fprodcllemf.1 φ1S
7 nfcv _jB
8 nfcsb1v _kj/kB
9 csbeq1a k=jB=j/kB
10 7 8 9 cbvprodi kAB=jAj/kB
11 5 ex φkABS
12 1 11 ralrimi φkABS
13 rspsbc jAkABS[˙j/k]˙BS
14 12 13 mpan9 φjA[˙j/k]˙BS
15 sbcel1g jV[˙j/k]˙BSj/kBS
16 15 elv [˙j/k]˙BSj/kBS
17 14 16 sylib φjAj/kBS
18 2 3 4 17 6 fprodcllem φjAj/kBS
19 10 18 eqeltrid φkABS