Step |
Hyp |
Ref |
Expression |
1 |
|
cncfcnvcn.j |
|- J = ( TopOpen ` CCfld ) |
2 |
|
cncfcnvcn.k |
|- K = ( J |`t X ) |
3 |
|
simpr |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> F e. ( X -cn-> Y ) ) |
4 |
|
cncfrss |
|- ( F e. ( X -cn-> Y ) -> X C_ CC ) |
5 |
4
|
adantl |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> X C_ CC ) |
6 |
|
cncfrss2 |
|- ( F e. ( X -cn-> Y ) -> Y C_ CC ) |
7 |
6
|
adantl |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> Y C_ CC ) |
8 |
|
eqid |
|- ( J |`t Y ) = ( J |`t Y ) |
9 |
1 2 8
|
cncfcn |
|- ( ( X C_ CC /\ Y C_ CC ) -> ( X -cn-> Y ) = ( K Cn ( J |`t Y ) ) ) |
10 |
5 7 9
|
syl2anc |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( X -cn-> Y ) = ( K Cn ( J |`t Y ) ) ) |
11 |
3 10
|
eleqtrd |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> F e. ( K Cn ( J |`t Y ) ) ) |
12 |
|
ishmeo |
|- ( F e. ( K Homeo ( J |`t Y ) ) <-> ( F e. ( K Cn ( J |`t Y ) ) /\ `' F e. ( ( J |`t Y ) Cn K ) ) ) |
13 |
12
|
baib |
|- ( F e. ( K Cn ( J |`t Y ) ) -> ( F e. ( K Homeo ( J |`t Y ) ) <-> `' F e. ( ( J |`t Y ) Cn K ) ) ) |
14 |
11 13
|
syl |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F e. ( K Homeo ( J |`t Y ) ) <-> `' F e. ( ( J |`t Y ) Cn K ) ) ) |
15 |
1
|
cnfldtop |
|- J e. Top |
16 |
1
|
cnfldtopon |
|- J e. ( TopOn ` CC ) |
17 |
16
|
toponunii |
|- CC = U. J |
18 |
17
|
restuni |
|- ( ( J e. Top /\ X C_ CC ) -> X = U. ( J |`t X ) ) |
19 |
15 5 18
|
sylancr |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> X = U. ( J |`t X ) ) |
20 |
2
|
unieqi |
|- U. K = U. ( J |`t X ) |
21 |
19 20
|
eqtr4di |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> X = U. K ) |
22 |
21
|
f1oeq2d |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> U. ( J |`t Y ) <-> F : U. K -1-1-onto-> U. ( J |`t Y ) ) ) |
23 |
17
|
restuni |
|- ( ( J e. Top /\ Y C_ CC ) -> Y = U. ( J |`t Y ) ) |
24 |
15 7 23
|
sylancr |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> Y = U. ( J |`t Y ) ) |
25 |
24
|
f1oeq3d |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> Y <-> F : X -1-1-onto-> U. ( J |`t Y ) ) ) |
26 |
|
simpl |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> K e. Comp ) |
27 |
1
|
cnfldhaus |
|- J e. Haus |
28 |
|
cnex |
|- CC e. _V |
29 |
28
|
ssex |
|- ( Y C_ CC -> Y e. _V ) |
30 |
7 29
|
syl |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> Y e. _V ) |
31 |
|
resthaus |
|- ( ( J e. Haus /\ Y e. _V ) -> ( J |`t Y ) e. Haus ) |
32 |
27 30 31
|
sylancr |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( J |`t Y ) e. Haus ) |
33 |
|
eqid |
|- U. K = U. K |
34 |
|
eqid |
|- U. ( J |`t Y ) = U. ( J |`t Y ) |
35 |
33 34
|
cmphaushmeo |
|- ( ( K e. Comp /\ ( J |`t Y ) e. Haus /\ F e. ( K Cn ( J |`t Y ) ) ) -> ( F e. ( K Homeo ( J |`t Y ) ) <-> F : U. K -1-1-onto-> U. ( J |`t Y ) ) ) |
36 |
26 32 11 35
|
syl3anc |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F e. ( K Homeo ( J |`t Y ) ) <-> F : U. K -1-1-onto-> U. ( J |`t Y ) ) ) |
37 |
22 25 36
|
3bitr4d |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> Y <-> F e. ( K Homeo ( J |`t Y ) ) ) ) |
38 |
1 8 2
|
cncfcn |
|- ( ( Y C_ CC /\ X C_ CC ) -> ( Y -cn-> X ) = ( ( J |`t Y ) Cn K ) ) |
39 |
7 5 38
|
syl2anc |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( Y -cn-> X ) = ( ( J |`t Y ) Cn K ) ) |
40 |
39
|
eleq2d |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( `' F e. ( Y -cn-> X ) <-> `' F e. ( ( J |`t Y ) Cn K ) ) ) |
41 |
14 37 40
|
3bitr4d |
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( Y -cn-> X ) ) ) |