Step |
Hyp |
Ref |
Expression |
1 |
|
iscn |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) ) |
2 |
1
|
simprbda |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> F : X --> Y ) |
3 |
|
eqid |
|- U. J = U. J |
4 |
3
|
cncnpi |
|- ( ( F e. ( J Cn K ) /\ x e. U. J ) -> F e. ( ( J CnP K ) ` x ) ) |
5 |
4
|
ralrimiva |
|- ( F e. ( J Cn K ) -> A. x e. U. J F e. ( ( J CnP K ) ` x ) ) |
6 |
5
|
adantl |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> A. x e. U. J F e. ( ( J CnP K ) ` x ) ) |
7 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
8 |
7
|
ad2antrr |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> X = U. J ) |
9 |
8
|
raleqdv |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> ( A. x e. X F e. ( ( J CnP K ) ` x ) <-> A. x e. U. J F e. ( ( J CnP K ) ` x ) ) ) |
10 |
6 9
|
mpbird |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> A. x e. X F e. ( ( J CnP K ) ` x ) ) |
11 |
2 10
|
jca |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) |
12 |
|
simprl |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) -> F : X --> Y ) |
13 |
|
cnvimass |
|- ( `' F " y ) C_ dom F |
14 |
|
fdm |
|- ( F : X --> Y -> dom F = X ) |
15 |
14
|
adantl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) -> dom F = X ) |
16 |
13 15
|
sseqtrid |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) -> ( `' F " y ) C_ X ) |
17 |
|
ssralv |
|- ( ( `' F " y ) C_ X -> ( A. x e. X F e. ( ( J CnP K ) ` x ) -> A. x e. ( `' F " y ) F e. ( ( J CnP K ) ` x ) ) ) |
18 |
16 17
|
syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) -> ( A. x e. X F e. ( ( J CnP K ) ` x ) -> A. x e. ( `' F " y ) F e. ( ( J CnP K ) ` x ) ) ) |
19 |
|
simprr |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) -> F e. ( ( J CnP K ) ` x ) ) |
20 |
|
simpllr |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) -> y e. K ) |
21 |
|
ffn |
|- ( F : X --> Y -> F Fn X ) |
22 |
21
|
ad2antlr |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) -> F Fn X ) |
23 |
|
simprl |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) -> x e. ( `' F " y ) ) |
24 |
|
elpreima |
|- ( F Fn X -> ( x e. ( `' F " y ) <-> ( x e. X /\ ( F ` x ) e. y ) ) ) |
25 |
24
|
simplbda |
|- ( ( F Fn X /\ x e. ( `' F " y ) ) -> ( F ` x ) e. y ) |
26 |
22 23 25
|
syl2anc |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) -> ( F ` x ) e. y ) |
27 |
|
cnpimaex |
|- ( ( F e. ( ( J CnP K ) ` x ) /\ y e. K /\ ( F ` x ) e. y ) -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) ) |
28 |
19 20 26 27
|
syl3anc |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) ) |
29 |
|
simpllr |
|- ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) /\ u e. J ) -> F : X --> Y ) |
30 |
29
|
ffund |
|- ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) /\ u e. J ) -> Fun F ) |
31 |
|
simp-4l |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) -> J e. ( TopOn ` X ) ) |
32 |
|
toponss |
|- ( ( J e. ( TopOn ` X ) /\ u e. J ) -> u C_ X ) |
33 |
31 32
|
sylan |
|- ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) /\ u e. J ) -> u C_ X ) |
34 |
29 14
|
syl |
|- ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) /\ u e. J ) -> dom F = X ) |
35 |
33 34
|
sseqtrrd |
|- ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) /\ u e. J ) -> u C_ dom F ) |
36 |
|
funimass3 |
|- ( ( Fun F /\ u C_ dom F ) -> ( ( F " u ) C_ y <-> u C_ ( `' F " y ) ) ) |
37 |
30 35 36
|
syl2anc |
|- ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) /\ u e. J ) -> ( ( F " u ) C_ y <-> u C_ ( `' F " y ) ) ) |
38 |
37
|
anbi2d |
|- ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) /\ u e. J ) -> ( ( x e. u /\ ( F " u ) C_ y ) <-> ( x e. u /\ u C_ ( `' F " y ) ) ) ) |
39 |
38
|
rexbidva |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) -> ( E. u e. J ( x e. u /\ ( F " u ) C_ y ) <-> E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) ) |
40 |
28 39
|
mpbid |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ ( x e. ( `' F " y ) /\ F e. ( ( J CnP K ) ` x ) ) ) -> E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) |
41 |
40
|
expr |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) /\ x e. ( `' F " y ) ) -> ( F e. ( ( J CnP K ) ` x ) -> E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) ) |
42 |
41
|
ralimdva |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) -> ( A. x e. ( `' F " y ) F e. ( ( J CnP K ) ` x ) -> A. x e. ( `' F " y ) E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) ) |
43 |
18 42
|
syld |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) -> ( A. x e. X F e. ( ( J CnP K ) ` x ) -> A. x e. ( `' F " y ) E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) ) |
44 |
43
|
impr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) -> A. x e. ( `' F " y ) E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) |
45 |
44
|
an32s |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) /\ y e. K ) -> A. x e. ( `' F " y ) E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) |
46 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
47 |
46
|
ad3antrrr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) /\ y e. K ) -> J e. Top ) |
48 |
|
eltop2 |
|- ( J e. Top -> ( ( `' F " y ) e. J <-> A. x e. ( `' F " y ) E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) ) |
49 |
47 48
|
syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) /\ y e. K ) -> ( ( `' F " y ) e. J <-> A. x e. ( `' F " y ) E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) ) |
50 |
45 49
|
mpbird |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) /\ y e. K ) -> ( `' F " y ) e. J ) |
51 |
50
|
ralrimiva |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) -> A. y e. K ( `' F " y ) e. J ) |
52 |
1
|
adantr |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) ) |
53 |
12 51 52
|
mpbir2and |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) -> F e. ( J Cn K ) ) |
54 |
11 53
|
impbida |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) ) |