Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- U. J = U. J |
2 |
1
|
jctr |
|- ( J e. Top -> ( J e. Top /\ U. J = U. J ) ) |
3 |
|
istopon |
|- ( J e. ( TopOn ` U. J ) <-> ( J e. Top /\ U. J = U. J ) ) |
4 |
2 3
|
sylibr |
|- ( J e. Top -> J e. ( TopOn ` U. J ) ) |
5 |
|
eqid |
|- U. K = U. K |
6 |
5
|
jctr |
|- ( K e. Top -> ( K e. Top /\ U. K = U. K ) ) |
7 |
|
istopon |
|- ( K e. ( TopOn ` U. K ) <-> ( K e. Top /\ U. K = U. K ) ) |
8 |
6 7
|
sylibr |
|- ( K e. Top -> K e. ( TopOn ` U. K ) ) |
9 |
|
cnfval |
|- ( ( J e. ( TopOn ` U. J ) /\ K e. ( TopOn ` U. K ) ) -> ( J Cn K ) = { f e. ( U. K ^m U. J ) | A. y e. K ( `' f " y ) e. J } ) |
10 |
4 8 9
|
syl2an |
|- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) = { f e. ( U. K ^m U. J ) | A. y e. K ( `' f " y ) e. J } ) |
11 |
|
uniexg |
|- ( K e. Top -> U. K e. _V ) |
12 |
|
uniexg |
|- ( J e. Top -> U. J e. _V ) |
13 |
|
mapvalg |
|- ( ( U. K e. _V /\ U. J e. _V ) -> ( U. K ^m U. J ) = { f | f : U. J --> U. K } ) |
14 |
11 12 13
|
syl2anr |
|- ( ( J e. Top /\ K e. Top ) -> ( U. K ^m U. J ) = { f | f : U. J --> U. K } ) |
15 |
|
mapex |
|- ( ( U. J e. _V /\ U. K e. _V ) -> { f | f : U. J --> U. K } e. _V ) |
16 |
12 11 15
|
syl2an |
|- ( ( J e. Top /\ K e. Top ) -> { f | f : U. J --> U. K } e. _V ) |
17 |
14 16
|
eqeltrd |
|- ( ( J e. Top /\ K e. Top ) -> ( U. K ^m U. J ) e. _V ) |
18 |
|
rabexg |
|- ( ( U. K ^m U. J ) e. _V -> { f e. ( U. K ^m U. J ) | A. y e. K ( `' f " y ) e. J } e. _V ) |
19 |
17 18
|
syl |
|- ( ( J e. Top /\ K e. Top ) -> { f e. ( U. K ^m U. J ) | A. y e. K ( `' f " y ) e. J } e. _V ) |
20 |
10 19
|
eqeltrd |
|- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V ) |