Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- U. J = U. J |
2 |
|
eqid |
|- U. K = U. K |
3 |
1 2
|
cnf |
|- ( F e. ( J Cn K ) -> F : U. J --> U. K ) |
4 |
3
|
adantr |
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> F : U. J --> U. K ) |
5 |
|
ffun |
|- ( F : U. J --> U. K -> Fun F ) |
6 |
|
funcnvcnv |
|- ( Fun F -> Fun `' `' F ) |
7 |
|
imadif |
|- ( Fun `' `' F -> ( `' F " ( U. K \ A ) ) = ( ( `' F " U. K ) \ ( `' F " A ) ) ) |
8 |
5 6 7
|
3syl |
|- ( F : U. J --> U. K -> ( `' F " ( U. K \ A ) ) = ( ( `' F " U. K ) \ ( `' F " A ) ) ) |
9 |
|
fimacnv |
|- ( F : U. J --> U. K -> ( `' F " U. K ) = U. J ) |
10 |
9
|
difeq1d |
|- ( F : U. J --> U. K -> ( ( `' F " U. K ) \ ( `' F " A ) ) = ( U. J \ ( `' F " A ) ) ) |
11 |
8 10
|
eqtr2d |
|- ( F : U. J --> U. K -> ( U. J \ ( `' F " A ) ) = ( `' F " ( U. K \ A ) ) ) |
12 |
4 11
|
syl |
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( U. J \ ( `' F " A ) ) = ( `' F " ( U. K \ A ) ) ) |
13 |
2
|
cldopn |
|- ( A e. ( Clsd ` K ) -> ( U. K \ A ) e. K ) |
14 |
|
cnima |
|- ( ( F e. ( J Cn K ) /\ ( U. K \ A ) e. K ) -> ( `' F " ( U. K \ A ) ) e. J ) |
15 |
13 14
|
sylan2 |
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( `' F " ( U. K \ A ) ) e. J ) |
16 |
12 15
|
eqeltrd |
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( U. J \ ( `' F " A ) ) e. J ) |
17 |
|
cntop1 |
|- ( F e. ( J Cn K ) -> J e. Top ) |
18 |
|
cnvimass |
|- ( `' F " A ) C_ dom F |
19 |
18 4
|
fssdm |
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( `' F " A ) C_ U. J ) |
20 |
1
|
iscld2 |
|- ( ( J e. Top /\ ( `' F " A ) C_ U. J ) -> ( ( `' F " A ) e. ( Clsd ` J ) <-> ( U. J \ ( `' F " A ) ) e. J ) ) |
21 |
17 19 20
|
syl2an2r |
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( ( `' F " A ) e. ( Clsd ` J ) <-> ( U. J \ ( `' F " A ) ) e. J ) ) |
22 |
16 21
|
mpbird |
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( `' F " A ) e. ( Clsd ` J ) ) |