Step |
Hyp |
Ref |
Expression |
1 |
|
cnmpt21.j |
|- ( ph -> J e. ( TopOn ` X ) ) |
2 |
|
cnmpt21.k |
|- ( ph -> K e. ( TopOn ` Y ) ) |
3 |
|
cnmpt2c.l |
|- ( ph -> L e. ( TopOn ` Z ) ) |
4 |
|
cnmpt2c.p |
|- ( ph -> P e. Z ) |
5 |
|
eqidd |
|- ( z = <. x , y >. -> P = P ) |
6 |
5
|
mpompt |
|- ( z e. ( X X. Y ) |-> P ) = ( x e. X , y e. Y |-> P ) |
7 |
|
txtopon |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) ) |
8 |
1 2 7
|
syl2anc |
|- ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) ) |
9 |
8 3 4
|
cnmptc |
|- ( ph -> ( z e. ( X X. Y ) |-> P ) e. ( ( J tX K ) Cn L ) ) |
10 |
6 9
|
eqeltrrid |
|- ( ph -> ( x e. X , y e. Y |-> P ) e. ( ( J tX K ) Cn L ) ) |