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