Step |
Hyp |
Ref |
Expression |
1 |
|
iscn.1 |
|- X = U. J |
2 |
|
iscn.2 |
|- Y = U. K |
3 |
|
df-cn |
|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } ) |
4 |
3
|
elmpocl |
|- ( F e. ( J Cn K ) -> ( J e. Top /\ K e. Top ) ) |
5 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` X ) ) |
6 |
2
|
toptopon |
|- ( K e. Top <-> K e. ( TopOn ` Y ) ) |
7 |
|
iscn |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) ) |
8 |
5 6 7
|
syl2anb |
|- ( ( J e. Top /\ K e. Top ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) ) |
9 |
4 8
|
biadanii |
|- ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) ) |