Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- U. J = U. J |
2 |
|
eqid |
|- U. K = U. K |
3 |
1 2
|
cnpf |
|- ( F e. ( ( J CnP K ) ` P ) -> F : U. J --> U. K ) |
4 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
5 |
4
|
feq2d |
|- ( J e. ( TopOn ` X ) -> ( F : X --> Y <-> F : U. J --> Y ) ) |
6 |
|
toponuni |
|- ( K e. ( TopOn ` Y ) -> Y = U. K ) |
7 |
6
|
feq3d |
|- ( K e. ( TopOn ` Y ) -> ( F : U. J --> Y <-> F : U. J --> U. K ) ) |
8 |
5 7
|
sylan9bb |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F : X --> Y <-> F : U. J --> U. K ) ) |
9 |
3 8
|
syl5ibr |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( ( J CnP K ) ` P ) -> F : X --> Y ) ) |
10 |
9
|
3impia |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y ) |