Step |
Hyp |
Ref |
Expression |
1 |
|
cnmpt21.j |
|- ( ph -> J e. ( TopOn ` X ) ) |
2 |
|
cnmpt21.k |
|- ( ph -> K e. ( TopOn ` Y ) ) |
3 |
|
cnmpt21.a |
|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) ) |
4 |
|
cnmpt2t.b |
|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) ) |
5 |
|
cnmpt22f.f |
|- ( ph -> F e. ( ( L tX M ) Cn N ) ) |
6 |
|
cntop2 |
|- ( ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) -> L e. Top ) |
7 |
3 6
|
syl |
|- ( ph -> L e. Top ) |
8 |
|
toptopon2 |
|- ( L e. Top <-> L e. ( TopOn ` U. L ) ) |
9 |
7 8
|
sylib |
|- ( ph -> L e. ( TopOn ` U. L ) ) |
10 |
|
cntop2 |
|- ( ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) -> M e. Top ) |
11 |
4 10
|
syl |
|- ( ph -> M e. Top ) |
12 |
|
toptopon2 |
|- ( M e. Top <-> M e. ( TopOn ` U. M ) ) |
13 |
11 12
|
sylib |
|- ( ph -> M e. ( TopOn ` U. M ) ) |
14 |
|
txtopon |
|- ( ( L e. ( TopOn ` U. L ) /\ M e. ( TopOn ` U. M ) ) -> ( L tX M ) e. ( TopOn ` ( U. L X. U. M ) ) ) |
15 |
9 13 14
|
syl2anc |
|- ( ph -> ( L tX M ) e. ( TopOn ` ( U. L X. U. M ) ) ) |
16 |
|
cntop2 |
|- ( F e. ( ( L tX M ) Cn N ) -> N e. Top ) |
17 |
5 16
|
syl |
|- ( ph -> N e. Top ) |
18 |
|
toptopon2 |
|- ( N e. Top <-> N e. ( TopOn ` U. N ) ) |
19 |
17 18
|
sylib |
|- ( ph -> N e. ( TopOn ` U. N ) ) |
20 |
|
cnf2 |
|- ( ( ( L tX M ) e. ( TopOn ` ( U. L X. U. M ) ) /\ N e. ( TopOn ` U. N ) /\ F e. ( ( L tX M ) Cn N ) ) -> F : ( U. L X. U. M ) --> U. N ) |
21 |
15 19 5 20
|
syl3anc |
|- ( ph -> F : ( U. L X. U. M ) --> U. N ) |
22 |
21
|
ffnd |
|- ( ph -> F Fn ( U. L X. U. M ) ) |
23 |
|
fnov |
|- ( F Fn ( U. L X. U. M ) <-> F = ( z e. U. L , w e. U. M |-> ( z F w ) ) ) |
24 |
22 23
|
sylib |
|- ( ph -> F = ( z e. U. L , w e. U. M |-> ( z F w ) ) ) |
25 |
24 5
|
eqeltrrd |
|- ( ph -> ( z e. U. L , w e. U. M |-> ( z F w ) ) e. ( ( L tX M ) Cn N ) ) |
26 |
|
oveq12 |
|- ( ( z = A /\ w = B ) -> ( z F w ) = ( A F B ) ) |
27 |
1 2 3 4 9 13 25 26
|
cnmpt22 |
|- ( ph -> ( x e. X , y e. Y |-> ( A F B ) ) e. ( ( J tX K ) Cn N ) ) |