Metamath Proof Explorer


Theorem fprodcllem

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

Ref Expression
Hypotheses fprodcllem.1 φ S
fprodcllem.2 φ x S y S x y S
fprodcllem.3 φ A Fin
fprodcllem.4 φ k A B S
fprodcllem.5 φ 1 S
Assertion fprodcllem φ k A B S

Proof

Step Hyp Ref Expression
1 fprodcllem.1 φ S
2 fprodcllem.2 φ x S y S x y S
3 fprodcllem.3 φ A Fin
4 fprodcllem.4 φ k A B S
5 fprodcllem.5 φ 1 S
6 prodeq1 A = k A B = k B
7 prod0 k B = 1
8 6 7 syl6eq A = k A B = 1
9 8 adantl φ A = k A B = 1
10 5 adantr φ A = 1 S
11 9 10 eqeltrd φ A = k A B S
12 1 adantr φ A S
13 2 adantlr φ A x S y S x y S
14 3 adantr φ A A Fin
15 4 adantlr φ A k A B S
16 simpr φ A A
17 12 13 14 15 16 fprodcl2lem φ A k A B S
18 11 17 pm2.61dane φ k A B S