Metamath Proof Explorer

Theorem cncls2

Description: Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion cncls2 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ~P Y ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` 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 Y -> x C_ Y )
4 3 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ x e. ~P Y ) -> x C_ Y )
5 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
6 5 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ x e. ~P Y ) -> Y = U. K )
7 4 6 sseqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ x e. ~P Y ) -> x C_ U. K )
8 eqid 
 |-  U. K = U. K
9 8 cncls2i 
 |-  ( ( F e. ( J Cn K ) /\ x C_ U. K ) -> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) )
10 9 expcom 
 |-  ( x C_ U. K -> ( F e. ( J Cn K ) -> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) )
11 7 10 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ x e. ~P Y ) -> ( F e. ( J Cn K ) -> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) )
12 11 ralrimdva 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) -> A. x e. ~P Y ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` 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 Y ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) ) )
14 8 cldss2 
 |-  ( Clsd ` K ) C_ ~P U. K
15 5 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> Y = U. K )
16 15 pweqd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ~P Y = ~P U. K )
17 14 16 sseqtrrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( Clsd ` K ) C_ ~P Y )
18 17 sseld 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( x e. ( Clsd ` K ) -> x e. ~P Y ) )
19 18 imim1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( x e. ~P Y -> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) -> ( x e. ( Clsd ` K ) -> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) ) )
20 cldcls 
 |-  ( x e. ( Clsd ` K ) -> ( ( cls ` K ) ` x ) = x )
21 20 ad2antll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> ( ( cls ` K ) ` x ) = x )
22 21 imaeq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> ( `' F " ( ( cls ` K ) ` x ) ) = ( `' F " x ) )
23 22 sseq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> ( ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) <-> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " x ) ) )
24 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
25 24 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> J e. Top )
26 cnvimass 
 |-  ( `' F " x ) C_ dom F
27 fdm 
 |-  ( F : X --> Y -> dom F = X )
28 27 ad2antrl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> dom F = X )
29 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
30 29 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> X = U. J )
31 28 30 eqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> dom F = U. J )
32 26 31 sseqtrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> ( `' F " x ) C_ U. J )
33 eqid 
 |-  U. J = U. J
34 33 iscld4 
 |-  ( ( J e. Top /\ ( `' F " x ) C_ U. J ) -> ( ( `' F " x ) e. ( Clsd ` J ) <-> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " x ) ) )
35 25 32 34 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> ( ( `' F " x ) e. ( Clsd ` J ) <-> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " x ) ) )
36 23 35 bitr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ x e. ( Clsd ` K ) ) ) -> ( ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) <-> ( `' F " x ) e. ( Clsd ` J ) ) )
37 36 expr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( x e. ( Clsd ` K ) -> ( ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) <-> ( `' F " x ) e. ( Clsd ` J ) ) ) )
38 37 pm5.74d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( x e. ( Clsd ` K ) -> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) <-> ( x e. ( Clsd ` K ) -> ( `' F " x ) e. ( Clsd ` J ) ) ) )
39 19 38 sylibd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( x e. ~P Y -> ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) -> ( x e. ( Clsd ` K ) -> ( `' F " x ) e. ( Clsd ` J ) ) ) )
40 39 ralimdv2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. ~P Y ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) -> A. x e. ( Clsd ` K ) ( `' F " x ) e. ( Clsd ` J ) ) )
41 40 imdistanda 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. x e. ~P Y ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) -> ( F : X --> Y /\ A. x e. ( Clsd ` K ) ( `' F " x ) e. ( Clsd ` J ) ) ) )
42 iscncl 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ( Clsd ` K ) ( `' F " x ) e. ( Clsd ` J ) ) ) )
43 41 42 sylibrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. x e. ~P Y ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) -> F e. ( J Cn K ) ) )
44 13 43 impbid 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ~P Y ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) ) )