Step |
Hyp |
Ref |
Expression |
1 |
|
cnf2 |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Cn K ) ) -> F : X --> Y ) |
2 |
1
|
3expia |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) -> F : X --> Y ) ) |
3 |
|
elpwi |
|- ( x e. ~P X -> x C_ X ) |
4 |
3
|
adantl |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ x e. ~P X ) -> x C_ X ) |
5 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
6 |
5
|
ad2antrr |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ x e. ~P X ) -> X = U. J ) |
7 |
4 6
|
sseqtrd |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ x e. ~P X ) -> x C_ U. J ) |
8 |
|
eqid |
|- U. J = U. J |
9 |
8
|
cnclsi |
|- ( ( F e. ( J Cn K ) /\ x C_ U. J ) -> ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) ) |
10 |
9
|
expcom |
|- ( x C_ U. J -> ( F e. ( J Cn K ) -> ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) ) ) |
11 |
7 10
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ x e. ~P X ) -> ( F e. ( J Cn K ) -> ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) ) ) |
12 |
11
|
ralrimdva |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) -> A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) ) ) |
13 |
2 12
|
jcad |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) -> ( F : X --> Y /\ A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) ) ) ) |
14 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
15 |
14
|
ad3antrrr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> X e. J ) |
16 |
|
cnvimass |
|- ( `' F " y ) C_ dom F |
17 |
|
fdm |
|- ( F : X --> Y -> dom F = X ) |
18 |
17
|
ad2antlr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> dom F = X ) |
19 |
16 18
|
sseqtrid |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( `' F " y ) C_ X ) |
20 |
15 19
|
sselpwd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( `' F " y ) e. ~P X ) |
21 |
|
fveq2 |
|- ( x = ( `' F " y ) -> ( ( cls ` J ) ` x ) = ( ( cls ` J ) ` ( `' F " y ) ) ) |
22 |
21
|
imaeq2d |
|- ( x = ( `' F " y ) -> ( F " ( ( cls ` J ) ` x ) ) = ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) ) |
23 |
|
imaeq2 |
|- ( x = ( `' F " y ) -> ( F " x ) = ( F " ( `' F " y ) ) ) |
24 |
23
|
fveq2d |
|- ( x = ( `' F " y ) -> ( ( cls ` K ) ` ( F " x ) ) = ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) ) |
25 |
22 24
|
sseq12d |
|- ( x = ( `' F " y ) -> ( ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) <-> ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) ) ) |
26 |
25
|
rspcv |
|- ( ( `' F " y ) e. ~P X -> ( A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) -> ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) ) ) |
27 |
20 26
|
syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) -> ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) ) ) |
28 |
|
topontop |
|- ( K e. ( TopOn ` Y ) -> K e. Top ) |
29 |
28
|
ad3antlr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> K e. Top ) |
30 |
|
elpwi |
|- ( y e. ~P Y -> y C_ Y ) |
31 |
30
|
adantl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> y C_ Y ) |
32 |
|
toponuni |
|- ( K e. ( TopOn ` Y ) -> Y = U. K ) |
33 |
32
|
ad3antlr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> Y = U. K ) |
34 |
31 33
|
sseqtrd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> y C_ U. K ) |
35 |
|
ffun |
|- ( F : X --> Y -> Fun F ) |
36 |
35
|
ad2antlr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> Fun F ) |
37 |
|
funimacnv |
|- ( Fun F -> ( F " ( `' F " y ) ) = ( y i^i ran F ) ) |
38 |
36 37
|
syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( F " ( `' F " y ) ) = ( y i^i ran F ) ) |
39 |
|
inss1 |
|- ( y i^i ran F ) C_ y |
40 |
38 39
|
eqsstrdi |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( F " ( `' F " y ) ) C_ y ) |
41 |
|
eqid |
|- U. K = U. K |
42 |
41
|
clsss |
|- ( ( K e. Top /\ y C_ U. K /\ ( F " ( `' F " y ) ) C_ y ) -> ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) C_ ( ( cls ` K ) ` y ) ) |
43 |
29 34 40 42
|
syl3anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) C_ ( ( cls ` K ) ` y ) ) |
44 |
|
sstr2 |
|- ( ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) -> ( ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) C_ ( ( cls ` K ) ` y ) -> ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` y ) ) ) |
45 |
43 44
|
syl5com |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) -> ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` y ) ) ) |
46 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
47 |
46
|
ad3antrrr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> J e. Top ) |
48 |
5
|
ad3antrrr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> X = U. J ) |
49 |
18 48
|
eqtrd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> dom F = U. J ) |
50 |
16 49
|
sseqtrid |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( `' F " y ) C_ U. J ) |
51 |
8
|
clsss3 |
|- ( ( J e. Top /\ ( `' F " y ) C_ U. J ) -> ( ( cls ` J ) ` ( `' F " y ) ) C_ U. J ) |
52 |
47 50 51
|
syl2anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( ( cls ` J ) ` ( `' F " y ) ) C_ U. J ) |
53 |
52 49
|
sseqtrrd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( ( cls ` J ) ` ( `' F " y ) ) C_ dom F ) |
54 |
|
funimass3 |
|- ( ( Fun F /\ ( ( cls ` J ) ` ( `' F " y ) ) C_ dom F ) -> ( ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` y ) <-> ( ( cls ` J ) ` ( `' F " y ) ) C_ ( `' F " ( ( cls ` K ) ` y ) ) ) ) |
55 |
36 53 54
|
syl2anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` y ) <-> ( ( cls ` J ) ` ( `' F " y ) ) C_ ( `' F " ( ( cls ` K ) ` y ) ) ) ) |
56 |
45 55
|
sylibd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( ( F " ( ( cls ` J ) ` ( `' F " y ) ) ) C_ ( ( cls ` K ) ` ( F " ( `' F " y ) ) ) -> ( ( cls ` J ) ` ( `' F " y ) ) C_ ( `' F " ( ( cls ` K ) ` y ) ) ) ) |
57 |
27 56
|
syld |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ y e. ~P Y ) -> ( A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) -> ( ( cls ` J ) ` ( `' F " y ) ) C_ ( `' F " ( ( cls ` K ) ` y ) ) ) ) |
58 |
57
|
ralrimdva |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) -> A. y e. ~P Y ( ( cls ` J ) ` ( `' F " y ) ) C_ ( `' F " ( ( cls ` K ) ` y ) ) ) ) |
59 |
58
|
imdistanda |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) ) -> ( F : X --> Y /\ A. y e. ~P Y ( ( cls ` J ) ` ( `' F " y ) ) C_ ( `' F " ( ( cls ` K ) ` y ) ) ) ) ) |
60 |
|
cncls2 |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ~P Y ( ( cls ` J ) ` ( `' F " y ) ) C_ ( `' F " ( ( cls ` K ) ` y ) ) ) ) ) |
61 |
59 60
|
sylibrd |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) ) -> F e. ( J Cn K ) ) ) |
62 |
13 61
|
impbid |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) ) ) ) |