Step |
Hyp |
Ref |
Expression |
1 |
|
paste.1 |
|- X = U. J |
2 |
|
paste.2 |
|- Y = U. K |
3 |
|
paste.4 |
|- ( ph -> A e. ( Clsd ` J ) ) |
4 |
|
paste.5 |
|- ( ph -> B e. ( Clsd ` J ) ) |
5 |
|
paste.6 |
|- ( ph -> ( A u. B ) = X ) |
6 |
|
paste.7 |
|- ( ph -> F : X --> Y ) |
7 |
|
paste.8 |
|- ( ph -> ( F |` A ) e. ( ( J |`t A ) Cn K ) ) |
8 |
|
paste.9 |
|- ( ph -> ( F |` B ) e. ( ( J |`t B ) Cn K ) ) |
9 |
5
|
ineq2d |
|- ( ph -> ( ( `' F " y ) i^i ( A u. B ) ) = ( ( `' F " y ) i^i X ) ) |
10 |
|
indi |
|- ( ( `' F " y ) i^i ( A u. B ) ) = ( ( ( `' F " y ) i^i A ) u. ( ( `' F " y ) i^i B ) ) |
11 |
6
|
ffund |
|- ( ph -> Fun F ) |
12 |
|
respreima |
|- ( Fun F -> ( `' ( F |` A ) " y ) = ( ( `' F " y ) i^i A ) ) |
13 |
|
respreima |
|- ( Fun F -> ( `' ( F |` B ) " y ) = ( ( `' F " y ) i^i B ) ) |
14 |
12 13
|
uneq12d |
|- ( Fun F -> ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) = ( ( ( `' F " y ) i^i A ) u. ( ( `' F " y ) i^i B ) ) ) |
15 |
11 14
|
syl |
|- ( ph -> ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) = ( ( ( `' F " y ) i^i A ) u. ( ( `' F " y ) i^i B ) ) ) |
16 |
10 15
|
eqtr4id |
|- ( ph -> ( ( `' F " y ) i^i ( A u. B ) ) = ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) ) |
17 |
|
imassrn |
|- ( `' F " y ) C_ ran `' F |
18 |
|
dfdm4 |
|- dom F = ran `' F |
19 |
|
fdm |
|- ( F : X --> Y -> dom F = X ) |
20 |
18 19
|
eqtr3id |
|- ( F : X --> Y -> ran `' F = X ) |
21 |
17 20
|
sseqtrid |
|- ( F : X --> Y -> ( `' F " y ) C_ X ) |
22 |
6 21
|
syl |
|- ( ph -> ( `' F " y ) C_ X ) |
23 |
|
df-ss |
|- ( ( `' F " y ) C_ X <-> ( ( `' F " y ) i^i X ) = ( `' F " y ) ) |
24 |
22 23
|
sylib |
|- ( ph -> ( ( `' F " y ) i^i X ) = ( `' F " y ) ) |
25 |
9 16 24
|
3eqtr3rd |
|- ( ph -> ( `' F " y ) = ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) ) |
26 |
25
|
adantr |
|- ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' F " y ) = ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) ) |
27 |
|
cnclima |
|- ( ( ( F |` A ) e. ( ( J |`t A ) Cn K ) /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` A ) " y ) e. ( Clsd ` ( J |`t A ) ) ) |
28 |
7 27
|
sylan |
|- ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` A ) " y ) e. ( Clsd ` ( J |`t A ) ) ) |
29 |
|
restcldr |
|- ( ( A e. ( Clsd ` J ) /\ ( `' ( F |` A ) " y ) e. ( Clsd ` ( J |`t A ) ) ) -> ( `' ( F |` A ) " y ) e. ( Clsd ` J ) ) |
30 |
3 28 29
|
syl2an2r |
|- ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` A ) " y ) e. ( Clsd ` J ) ) |
31 |
|
cnclima |
|- ( ( ( F |` B ) e. ( ( J |`t B ) Cn K ) /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` B ) " y ) e. ( Clsd ` ( J |`t B ) ) ) |
32 |
8 31
|
sylan |
|- ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` B ) " y ) e. ( Clsd ` ( J |`t B ) ) ) |
33 |
|
restcldr |
|- ( ( B e. ( Clsd ` J ) /\ ( `' ( F |` B ) " y ) e. ( Clsd ` ( J |`t B ) ) ) -> ( `' ( F |` B ) " y ) e. ( Clsd ` J ) ) |
34 |
4 32 33
|
syl2an2r |
|- ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` B ) " y ) e. ( Clsd ` J ) ) |
35 |
|
uncld |
|- ( ( ( `' ( F |` A ) " y ) e. ( Clsd ` J ) /\ ( `' ( F |` B ) " y ) e. ( Clsd ` J ) ) -> ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) e. ( Clsd ` J ) ) |
36 |
30 34 35
|
syl2anc |
|- ( ( ph /\ y e. ( Clsd ` K ) ) -> ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) e. ( Clsd ` J ) ) |
37 |
26 36
|
eqeltrd |
|- ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' F " y ) e. ( Clsd ` J ) ) |
38 |
37
|
ralrimiva |
|- ( ph -> A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) |
39 |
|
cldrcl |
|- ( A e. ( Clsd ` J ) -> J e. Top ) |
40 |
3 39
|
syl |
|- ( ph -> J e. Top ) |
41 |
|
cntop2 |
|- ( ( F |` A ) e. ( ( J |`t A ) Cn K ) -> K e. Top ) |
42 |
7 41
|
syl |
|- ( ph -> K e. Top ) |
43 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` X ) ) |
44 |
2
|
toptopon |
|- ( K e. Top <-> K e. ( TopOn ` Y ) ) |
45 |
|
iscncl |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) ) |
46 |
43 44 45
|
syl2anb |
|- ( ( J e. Top /\ K e. Top ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) ) |
47 |
40 42 46
|
syl2anc |
|- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) ) |
48 |
6 38 47
|
mpbir2and |
|- ( ph -> F e. ( J Cn K ) ) |