Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> J e. Comp ) |
2 |
|
eqid |
|- U. J = U. J |
3 |
|
eqid |
|- U. K = U. K |
4 |
2 3
|
cnf |
|- ( F e. ( J Cn K ) -> F : U. J --> U. K ) |
5 |
4
|
adantl |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F : U. J --> U. K ) |
6 |
5
|
ffnd |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F Fn U. J ) |
7 |
|
dffn4 |
|- ( F Fn U. J <-> F : U. J -onto-> ran F ) |
8 |
6 7
|
sylib |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F : U. J -onto-> ran F ) |
9 |
|
cntop2 |
|- ( F e. ( J Cn K ) -> K e. Top ) |
10 |
9
|
adantl |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> K e. Top ) |
11 |
5
|
frnd |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ran F C_ U. K ) |
12 |
3
|
restuni |
|- ( ( K e. Top /\ ran F C_ U. K ) -> ran F = U. ( K |`t ran F ) ) |
13 |
10 11 12
|
syl2anc |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ran F = U. ( K |`t ran F ) ) |
14 |
|
foeq3 |
|- ( ran F = U. ( K |`t ran F ) -> ( F : U. J -onto-> ran F <-> F : U. J -onto-> U. ( K |`t ran F ) ) ) |
15 |
13 14
|
syl |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ( F : U. J -onto-> ran F <-> F : U. J -onto-> U. ( K |`t ran F ) ) ) |
16 |
8 15
|
mpbid |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F : U. J -onto-> U. ( K |`t ran F ) ) |
17 |
|
simpr |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F e. ( J Cn K ) ) |
18 |
|
toptopon2 |
|- ( K e. Top <-> K e. ( TopOn ` U. K ) ) |
19 |
10 18
|
sylib |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> K e. ( TopOn ` U. K ) ) |
20 |
|
ssidd |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ran F C_ ran F ) |
21 |
|
cnrest2 |
|- ( ( K e. ( TopOn ` U. K ) /\ ran F C_ ran F /\ ran F C_ U. K ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t ran F ) ) ) ) |
22 |
19 20 11 21
|
syl3anc |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K |`t ran F ) ) ) ) |
23 |
17 22
|
mpbid |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> F e. ( J Cn ( K |`t ran F ) ) ) |
24 |
|
eqid |
|- U. ( K |`t ran F ) = U. ( K |`t ran F ) |
25 |
24
|
cncmp |
|- ( ( J e. Comp /\ F : U. J -onto-> U. ( K |`t ran F ) /\ F e. ( J Cn ( K |`t ran F ) ) ) -> ( K |`t ran F ) e. Comp ) |
26 |
1 16 23 25
|
syl3anc |
|- ( ( J e. Comp /\ F e. ( J Cn K ) ) -> ( K |`t ran F ) e. Comp ) |