Metamath Proof Explorer

Theorem cncls

Description: Continuity in terms of closure. (Contributed by Jeff Hankins, 1-Oct-2009) (Proof shortened by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion cncls 
|- ( ( 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 ) ) ) ) )

Proof

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 ) ) ) ) )