Step |
Hyp |
Ref |
Expression |
1 |
|
fprodcllem.1 |
|- ( ph -> S C_ CC ) |
2 |
|
fprodcllem.2 |
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S ) |
3 |
|
fprodcllem.3 |
|- ( ph -> A e. Fin ) |
4 |
|
fprodcllem.4 |
|- ( ( ph /\ k e. A ) -> B e. S ) |
5 |
|
fprodcl2lem.5 |
|- ( ph -> A =/= (/) ) |
6 |
5
|
a1d |
|- ( ph -> ( -. prod_ k e. A B e. S -> A =/= (/) ) ) |
7 |
6
|
necon4bd |
|- ( ph -> ( A = (/) -> prod_ k e. A B e. S ) ) |
8 |
|
prodfc |
|- prod_ m e. A ( ( k e. A |-> B ) ` m ) = prod_ k e. A B |
9 |
|
fveq2 |
|- ( m = ( f ` x ) -> ( ( k e. A |-> B ) ` m ) = ( ( k e. A |-> B ) ` ( f ` x ) ) ) |
10 |
|
simprl |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN ) |
11 |
|
simprr |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) |
12 |
1
|
adantr |
|- ( ( ph /\ k e. A ) -> S C_ CC ) |
13 |
12 4
|
sseldd |
|- ( ( ph /\ k e. A ) -> B e. CC ) |
14 |
13
|
fmpttd |
|- ( ph -> ( k e. A |-> B ) : A --> CC ) |
15 |
14
|
ffvelrnda |
|- ( ( ph /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC ) |
16 |
15
|
adantlr |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC ) |
17 |
|
f1of |
|- ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A ) |
18 |
17
|
ad2antll |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A ) |
19 |
|
fvco3 |
|- ( ( f : ( 1 ... ( # ` A ) ) --> A /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) = ( ( k e. A |-> B ) ` ( f ` x ) ) ) |
20 |
18 19
|
sylan |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) = ( ( k e. A |-> B ) ` ( f ` x ) ) ) |
21 |
9 10 11 16 20
|
fprod |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> B ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) ) |
22 |
8 21
|
eqtr3id |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B = ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) ) |
23 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
24 |
10 23
|
eleqtrdi |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. ( ZZ>= ` 1 ) ) |
25 |
4
|
fmpttd |
|- ( ph -> ( k e. A |-> B ) : A --> S ) |
26 |
|
fco |
|- ( ( ( k e. A |-> B ) : A --> S /\ f : ( 1 ... ( # ` A ) ) --> A ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> S ) |
27 |
25 18 26
|
syl2an2r |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> S ) |
28 |
27
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) e. S ) |
29 |
2
|
adantlr |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S ) |
30 |
24 28 29
|
seqcl |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) e. S ) |
31 |
22 30
|
eqeltrd |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B e. S ) |
32 |
31
|
expr |
|- ( ( ph /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B e. S ) ) |
33 |
32
|
exlimdv |
|- ( ( ph /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B e. S ) ) |
34 |
33
|
expimpd |
|- ( ph -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A B e. S ) ) |
35 |
|
fz1f1o |
|- ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) ) |
36 |
3 35
|
syl |
|- ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) ) |
37 |
7 34 36
|
mpjaod |
|- ( ph -> prod_ k e. A B e. S ) |