| Step |
Hyp |
Ref |
Expression |
| 1 |
|
imasubclem1.f |
|- ( ph -> F e. V ) |
| 2 |
|
imasubclem1.g |
|- ( ph -> G e. W ) |
| 3 |
|
imasubclem3.x |
|- ( ph -> X e. A ) |
| 4 |
|
imasubclem3.y |
|- ( ph -> Y e. B ) |
| 5 |
|
imasubclem3.k |
|- K = ( x e. A , y e. B |-> U_ z e. ( ( `' F " { x } ) X. ( `' G " { y } ) ) ( ( H ` C ) " D ) ) |
| 6 |
1 2
|
imasubclem1 |
|- ( ph -> U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) e. _V ) |
| 7 |
|
simpl |
|- ( ( x = X /\ y = Y ) -> x = X ) |
| 8 |
7
|
sneqd |
|- ( ( x = X /\ y = Y ) -> { x } = { X } ) |
| 9 |
8
|
imaeq2d |
|- ( ( x = X /\ y = Y ) -> ( `' F " { x } ) = ( `' F " { X } ) ) |
| 10 |
|
simpr |
|- ( ( x = X /\ y = Y ) -> y = Y ) |
| 11 |
10
|
sneqd |
|- ( ( x = X /\ y = Y ) -> { y } = { Y } ) |
| 12 |
11
|
imaeq2d |
|- ( ( x = X /\ y = Y ) -> ( `' G " { y } ) = ( `' G " { Y } ) ) |
| 13 |
9 12
|
xpeq12d |
|- ( ( x = X /\ y = Y ) -> ( ( `' F " { x } ) X. ( `' G " { y } ) ) = ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ) |
| 14 |
13
|
iuneq1d |
|- ( ( x = X /\ y = Y ) -> U_ z e. ( ( `' F " { x } ) X. ( `' G " { y } ) ) ( ( H ` C ) " D ) = U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) ) |
| 15 |
14 5
|
ovmpoga |
|- ( ( X e. A /\ Y e. B /\ U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) e. _V ) -> ( X K Y ) = U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) ) |
| 16 |
3 4 6 15
|
syl3anc |
|- ( ph -> ( X K Y ) = U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) ) |