Metamath Proof Explorer


Theorem fprodcl2lem

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
fprodcl2lem.5 φ A
Assertion fprodcl2lem φ 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 fprodcl2lem.5 φ A
6 5 a1d φ ¬ k A B S A
7 6 necon4bd φ A = k A B S
8 prodfc m A k A B m = k A B
9 fveq2 m = f x k A B m = k A B f x
10 simprl φ A f : 1 A 1-1 onto A A
11 simprr φ A f : 1 A 1-1 onto A f : 1 A 1-1 onto A
12 1 adantr φ k A S
13 12 4 sseldd φ k A B
14 13 fmpttd φ k A B : A
15 14 ffvelrnda φ m A k A B m
16 15 adantlr φ A f : 1 A 1-1 onto A m A k A B m
17 f1of f : 1 A 1-1 onto A f : 1 A A
18 17 ad2antll φ A f : 1 A 1-1 onto A f : 1 A A
19 fvco3 f : 1 A A x 1 A k A B f x = k A B f x
20 18 19 sylan φ A f : 1 A 1-1 onto A x 1 A k A B f x = k A B f x
21 9 10 11 16 20 fprod φ A f : 1 A 1-1 onto A m A k A B m = seq 1 × k A B f A
22 8 21 eqtr3id φ A f : 1 A 1-1 onto A k A B = seq 1 × k A B f A
23 nnuz = 1
24 10 23 eleqtrdi φ A f : 1 A 1-1 onto A A 1
25 4 fmpttd φ k A B : A S
26 fco k A B : A S f : 1 A A k A B f : 1 A S
27 25 18 26 syl2an2r φ A f : 1 A 1-1 onto A k A B f : 1 A S
28 27 ffvelrnda φ A f : 1 A 1-1 onto A x 1 A k A B f x S
29 2 adantlr φ A f : 1 A 1-1 onto A x S y S x y S
30 24 28 29 seqcl φ A f : 1 A 1-1 onto A seq 1 × k A B f A S
31 22 30 eqeltrd φ A f : 1 A 1-1 onto A k A B S
32 31 expr φ A f : 1 A 1-1 onto A k A B S
33 32 exlimdv φ A f f : 1 A 1-1 onto A k A B S
34 33 expimpd φ A f f : 1 A 1-1 onto A k A B S
35 fz1f1o A Fin A = A f f : 1 A 1-1 onto A
36 3 35 syl φ A = A f f : 1 A 1-1 onto A
37 7 34 36 mpjaod φ k A B S