| Step |
Hyp |
Ref |
Expression |
| 1 |
|
imasubclem1.f |
|- ( ph -> F e. V ) |
| 2 |
|
imasubclem1.g |
|- ( ph -> G e. W ) |
| 3 |
|
imasubclem2.k |
|- K = ( y e. X , z e. Y |-> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) ) |
| 4 |
1 2
|
imasubclem1 |
|- ( ph -> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V ) |
| 5 |
4
|
adantr |
|- ( ( ph /\ ( y e. X /\ z e. Y ) ) -> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V ) |
| 6 |
5
|
ralrimivva |
|- ( ph -> A. y e. X A. z e. Y U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V ) |
| 7 |
3
|
fnmpo |
|- ( A. y e. X A. z e. Y U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V -> K Fn ( X X. Y ) ) |
| 8 |
6 7
|
syl |
|- ( ph -> K Fn ( X X. Y ) ) |