Step |
Hyp |
Ref |
Expression |
1 |
|
fprodxp.1 |
|- ( z = <. j , k >. -> D = C ) |
2 |
|
fprodxp.2 |
|- ( ph -> A e. Fin ) |
3 |
|
fprodxp.3 |
|- ( ph -> B e. Fin ) |
4 |
|
fprodxp.4 |
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC ) |
5 |
3
|
adantr |
|- ( ( ph /\ j e. A ) -> B e. Fin ) |
6 |
1 2 5 4
|
fprod2d |
|- ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D ) |
7 |
|
iunxpconst |
|- U_ j e. A ( { j } X. B ) = ( A X. B ) |
8 |
7
|
prodeq1i |
|- prod_ z e. U_ j e. A ( { j } X. B ) D = prod_ z e. ( A X. B ) D |
9 |
6 8
|
eqtrdi |
|- ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. ( A X. B ) D ) |