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

Metamath Proof Explorer

Theorem fprodss

Description: Change the index set to a subset in a finite product. (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Hypotheses fprodss.1 
|- ( ph -> A C_ B )
fprodss.2 
|- ( ( ph /\ k e. A ) -> C e. CC )
fprodss.3 
|- ( ( ph /\ k e. ( B \ A ) ) -> C = 1 )
fprodss.4 
|- ( ph -> B e. Fin )
Assertion fprodss 
|- ( ph -> prod_ k e. A C = prod_ k e. B C )

Proof

Step Hyp Ref Expression
1 fprodss.1 
 |-  ( ph -> A C_ B )
2 fprodss.2 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
3 fprodss.3 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C = 1 )
4 fprodss.4 
 |-  ( ph -> B e. Fin )
5 sseq2 
 |-  ( B = (/) -> ( A C_ B <-> A C_ (/) ) )
6 ss0 
 |-  ( A C_ (/) -> A = (/) )
7 5 6 biimtrdi 
 |-  ( B = (/) -> ( A C_ B -> A = (/) ) )
8 prodeq1 
 |-  ( A = (/) -> prod_ k e. A C = prod_ k e. (/) C )
9 prodeq1 
 |-  ( B = (/) -> prod_ k e. B C = prod_ k e. (/) C )
10 9 eqcomd 
 |-  ( B = (/) -> prod_ k e. (/) C = prod_ k e. B C )
11 8 10 sylan9eq 
 |-  ( ( A = (/) /\ B = (/) ) -> prod_ k e. A C = prod_ k e. B C )
12 11 expcom 
 |-  ( B = (/) -> ( A = (/) -> prod_ k e. A C = prod_ k e. B C ) )
13 7 12 syld 
 |-  ( B = (/) -> ( A C_ B -> prod_ k e. A C = prod_ k e. B C ) )
14 1 13 syl5com 
 |-  ( ph -> ( B = (/) -> prod_ k e. A C = prod_ k e. B C ) )
15 cnvimass 
 |-  ( `' f " A ) C_ dom f
16 simprr 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> f : ( 1 ... ( # ` B ) ) -1-1-onto-> B )
17 f1of 
 |-  ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> f : ( 1 ... ( # ` B ) ) --> B )
18 16 17 syl 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> f : ( 1 ... ( # ` B ) ) --> B )
19 15 18 fssdm 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( `' f " A ) C_ ( 1 ... ( # ` B ) ) )
20 f1ofn 
 |-  ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> f Fn ( 1 ... ( # ` B ) ) )
21 elpreima 
 |-  ( f Fn ( 1 ... ( # ` B ) ) -> ( n e. ( `' f " A ) <-> ( n e. ( 1 ... ( # ` B ) ) /\ ( f ` n ) e. A ) ) )
22 16 20 21 3syl 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( n e. ( `' f " A ) <-> ( n e. ( 1 ... ( # ` B ) ) /\ ( f ` n ) e. A ) ) )
23 18 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( 1 ... ( # ` B ) ) ) -> ( f ` n ) e. B )
24 23 ex 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( n e. ( 1 ... ( # ` B ) ) -> ( f ` n ) e. B ) )
25 24 adantrd 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( ( n e. ( 1 ... ( # ` B ) ) /\ ( f ` n ) e. A ) -> ( f ` n ) e. B ) )
26 22 25 sylbid 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( n e. ( `' f " A ) -> ( f ` n ) e. B ) )
27 26 imp 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( `' f " A ) ) -> ( f ` n ) e. B )
28 2 ex 
 |-  ( ph -> ( k e. A -> C e. CC ) )
29 28 adantr 
 |-  ( ( ph /\ k e. B ) -> ( k e. A -> C e. CC ) )
30 eldif 
 |-  ( k e. ( B \ A ) <-> ( k e. B /\ -. k e. A ) )
31 ax-1cn 
 |-  1 e. CC
32 3 31 eqeltrdi 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C e. CC )
33 30 32 sylan2br 
 |-  ( ( ph /\ ( k e. B /\ -. k e. A ) ) -> C e. CC )
34 33 expr 
 |-  ( ( ph /\ k e. B ) -> ( -. k e. A -> C e. CC ) )
35 29 34 pm2.61d 
 |-  ( ( ph /\ k e. B ) -> C e. CC )
36 35 adantlr 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ k e. B ) -> C e. CC )
37 36 fmpttd 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( k e. B |-> C ) : B --> CC )
38 37 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ ( f ` n ) e. B ) -> ( ( k e. B |-> C ) ` ( f ` n ) ) e. CC )
39 27 38 syldan 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( `' f " A ) ) -> ( ( k e. B |-> C ) ` ( f ` n ) ) e. CC )
40 eqid 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` 1 )
41 simprl 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( # ` B ) e. NN )
42 nnuz 
 |-  NN = ( ZZ>= ` 1 )
43 41 42 eleqtrdi 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( # ` B ) e. ( ZZ>= ` 1 ) )
44 ssidd 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( 1 ... ( # ` B ) ) C_ ( 1 ... ( # ` B ) ) )
45 40 43 44 fprodntriv 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> E. m e. ( ZZ>= ` 1 ) E. y ( y =/= 0 /\ seq m ( x. , ( n e. ( ZZ>= ` 1 ) |-> if ( n e. ( 1 ... ( # ` B ) ) , ( ( k e. B |-> C ) ` ( f ` n ) ) , 1 ) ) ) ~~> y ) )
46 eldifi 
 |-  ( n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) -> n e. ( 1 ... ( # ` B ) ) )
47 46 23 sylan2 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( f ` n ) e. B )
48 eldifn 
 |-  ( n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) -> -. n e. ( `' f " A ) )
49 48 adantl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> -. n e. ( `' f " A ) )
50 46 adantl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> n e. ( 1 ... ( # ` B ) ) )
51 22 adantr 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( n e. ( `' f " A ) <-> ( n e. ( 1 ... ( # ` B ) ) /\ ( f ` n ) e. A ) ) )
52 50 51 mpbirand 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( n e. ( `' f " A ) <-> ( f ` n ) e. A ) )
53 49 52 mtbid 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> -. ( f ` n ) e. A )
54 47 53 eldifd 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( f ` n ) e. ( B \ A ) )
55 difss 
 |-  ( B \ A ) C_ B
56 resmpt 
 |-  ( ( B \ A ) C_ B -> ( ( k e. B |-> C ) |` ( B \ A ) ) = ( k e. ( B \ A ) |-> C ) )
57 55 56 ax-mp 
 |-  ( ( k e. B |-> C ) |` ( B \ A ) ) = ( k e. ( B \ A ) |-> C )
58 57 fveq1i 
 |-  ( ( ( k e. B |-> C ) |` ( B \ A ) ) ` ( f ` n ) ) = ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) )
59 fvres 
 |-  ( ( f ` n ) e. ( B \ A ) -> ( ( ( k e. B |-> C ) |` ( B \ A ) ) ` ( f ` n ) ) = ( ( k e. B |-> C ) ` ( f ` n ) ) )
60 58 59 eqtr3id 
 |-  ( ( f ` n ) e. ( B \ A ) -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) = ( ( k e. B |-> C ) ` ( f ` n ) ) )
61 54 60 syl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) = ( ( k e. B |-> C ) ` ( f ` n ) ) )
62 1ex 
 |-  1 e. _V
63 62 elsn2 
 |-  ( C e. { 1 } <-> C = 1 )
64 3 63 sylibr 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C e. { 1 } )
65 64 fmpttd 
 |-  ( ph -> ( k e. ( B \ A ) |-> C ) : ( B \ A ) --> { 1 } )
66 65 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( k e. ( B \ A ) |-> C ) : ( B \ A ) --> { 1 } )
67 66 54 ffvelcdmd 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) e. { 1 } )
68 elsni 
 |-  ( ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) e. { 1 } -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) = 1 )
69 67 68 syl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( ( k e. ( B \ A ) |-> C ) ` ( f ` n ) ) = 1 )
70 61 69 eqtr3d 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( ( 1 ... ( # ` B ) ) \ ( `' f " A ) ) ) -> ( ( k e. B |-> C ) ` ( f ` n ) ) = 1 )
71 fzssuz 
 |-  ( 1 ... ( # ` B ) ) C_ ( ZZ>= ` 1 )
72 71 a1i 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( 1 ... ( # ` B ) ) C_ ( ZZ>= ` 1 ) )
73 19 39 45 70 72 prodss 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> prod_ n e. ( `' f " A ) ( ( k e. B |-> C ) ` ( f ` n ) ) = prod_ n e. ( 1 ... ( # ` B ) ) ( ( k e. B |-> C ) ` ( f ` n ) ) )
74 1 adantr 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> A C_ B )
75 74 resmptd 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( ( k e. B |-> C ) |` A ) = ( k e. A |-> C ) )
76 75 fveq1d 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( ( ( k e. B |-> C ) |` A ) ` m ) = ( ( k e. A |-> C ) ` m ) )
77 fvres 
 |-  ( m e. A -> ( ( ( k e. B |-> C ) |` A ) ` m ) = ( ( k e. B |-> C ) ` m ) )
78 76 77 sylan9req 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> ( ( k e. A |-> C ) ` m ) = ( ( k e. B |-> C ) ` m ) )
79 78 prodeq2dv 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> prod_ m e. A ( ( k e. A |-> C ) ` m ) = prod_ m e. A ( ( k e. B |-> C ) ` m ) )
80 fveq2 
 |-  ( m = ( f ` n ) -> ( ( k e. B |-> C ) ` m ) = ( ( k e. B |-> C ) ` ( f ` n ) ) )
81 fzfid 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( 1 ... ( # ` B ) ) e. Fin )
82 81 18 fisuppfi 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( `' f " A ) e. Fin )
83 f1of1 
 |-  ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> f : ( 1 ... ( # ` B ) ) -1-1-> B )
84 16 83 syl 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> f : ( 1 ... ( # ` B ) ) -1-1-> B )
85 f1ores 
 |-  ( ( f : ( 1 ... ( # ` B ) ) -1-1-> B /\ ( `' f " A ) C_ ( 1 ... ( # ` B ) ) ) -> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> ( f " ( `' f " A ) ) )
86 84 19 85 syl2anc 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> ( f " ( `' f " A ) ) )
87 f1ofo 
 |-  ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> f : ( 1 ... ( # ` B ) ) -onto-> B )
88 16 87 syl 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> f : ( 1 ... ( # ` B ) ) -onto-> B )
89 foimacnv 
 |-  ( ( f : ( 1 ... ( # ` B ) ) -onto-> B /\ A C_ B ) -> ( f " ( `' f " A ) ) = A )
90 88 74 89 syl2anc 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( f " ( `' f " A ) ) = A )
91 90 f1oeq3d 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> ( f " ( `' f " A ) ) <-> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> A ) )
92 86 91 mpbid 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> ( f |` ( `' f " A ) ) : ( `' f " A ) -1-1-onto-> A )
93 fvres 
 |-  ( n e. ( `' f " A ) -> ( ( f |` ( `' f " A ) ) ` n ) = ( f ` n ) )
94 93 adantl 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( `' f " A ) ) -> ( ( f |` ( `' f " A ) ) ` n ) = ( f ` n ) )
95 74 sselda 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> m e. B )
96 37 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. B ) -> ( ( k e. B |-> C ) ` m ) e. CC )
97 95 96 syldan 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ m e. A ) -> ( ( k e. B |-> C ) ` m ) e. CC )
98 80 82 92 94 97 fprodf1o 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> prod_ m e. A ( ( k e. B |-> C ) ` m ) = prod_ n e. ( `' f " A ) ( ( k e. B |-> C ) ` ( f ` n ) ) )
99 79 98 eqtrd 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> prod_ m e. A ( ( k e. A |-> C ) ` m ) = prod_ n e. ( `' f " A ) ( ( k e. B |-> C ) ` ( f ` n ) ) )
100 eqidd 
 |-  ( ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) /\ n e. ( 1 ... ( # ` B ) ) ) -> ( f ` n ) = ( f ` n ) )
101 80 81 16 100 96 fprodf1o 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> prod_ m e. B ( ( k e. B |-> C ) ` m ) = prod_ n e. ( 1 ... ( # ` B ) ) ( ( k e. B |-> C ) ` ( f ` n ) ) )
102 73 99 101 3eqtr4d 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> prod_ m e. A ( ( k e. A |-> C ) ` m ) = prod_ m e. B ( ( k e. B |-> C ) ` m ) )
103 prodfc 
 |-  prod_ m e. A ( ( k e. A |-> C ) ` m ) = prod_ k e. A C
104 prodfc 
 |-  prod_ m e. B ( ( k e. B |-> C ) ` m ) = prod_ k e. B C
105 102 103 104 3eqtr3g 
 |-  ( ( ph /\ ( ( # ` B ) e. NN /\ f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) -> prod_ k e. A C = prod_ k e. B C )
106 105 expr 
 |-  ( ( ph /\ ( # ` B ) e. NN ) -> ( f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> prod_ k e. A C = prod_ k e. B C ) )
107 106 exlimdv 
 |-  ( ( ph /\ ( # ` B ) e. NN ) -> ( E. f f : ( 1 ... ( # ` B ) ) -1-1-onto-> B -> prod_ k e. A C = prod_ k e. B C ) )
108 107 expimpd 
 |-  ( ph -> ( ( ( # ` B ) e. NN /\ E. f f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) -> prod_ k e. A C = prod_ k e. B C ) )
109 fz1f1o 
 |-  ( B e. Fin -> ( B = (/) \/ ( ( # ` B ) e. NN /\ E. f f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) )
110 4 109 syl 
 |-  ( ph -> ( B = (/) \/ ( ( # ` B ) e. NN /\ E. f f : ( 1 ... ( # ` B ) ) -1-1-onto-> B ) ) )
111 14 108 110 mpjaod 
 |-  ( ph -> prod_ k e. A C = prod_ k e. B C )