Metamath Proof Explorer

Theorem cnntr

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

Ref Expression
Assertion cnntr 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ~P Y ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' 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 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 cnntri 
 |-  ( ( F e. ( J Cn K ) /\ x C_ U. K ) -> ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) )
10 9 expcom 
 |-  ( x C_ U. K -> ( F e. ( J Cn K ) -> ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) )
11 7 10 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ x e. ~P Y ) -> ( F e. ( J Cn K ) -> ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) )
12 11 ralrimdva 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) -> A. x e. ~P Y ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' 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 Y ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) ) )
14 toponss 
 |-  ( ( K e. ( TopOn ` Y ) /\ x e. K ) -> x C_ Y )
15 velpw 
 |-  ( x e. ~P Y <-> x C_ Y )
16 14 15 sylibr 
 |-  ( ( K e. ( TopOn ` Y ) /\ x e. K ) -> x e. ~P Y )
17 16 ex 
 |-  ( K e. ( TopOn ` Y ) -> ( x e. K -> x e. ~P Y ) )
18 17 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( x e. K -> x e. ~P Y ) )
19 18 imim1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( x e. ~P Y -> ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) -> ( x e. K -> ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) ) )
20 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
21 20 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> J e. Top )
22 cnvimass 
 |-  ( `' F " x ) C_ dom F
23 fdm 
 |-  ( F : X --> Y -> dom F = X )
24 23 ad2antlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> dom F = X )
25 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
26 25 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> X = U. J )
27 24 26 eqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> dom F = U. J )
28 22 27 sseqtrid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> ( `' F " x ) C_ U. J )
29 eqid 
 |-  U. J = U. J
30 29 ntrss2 
 |-  ( ( J e. Top /\ ( `' F " x ) C_ U. J ) -> ( ( int ` J ) ` ( `' F " x ) ) C_ ( `' F " x ) )
31 21 28 30 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> ( ( int ` J ) ` ( `' F " x ) ) C_ ( `' F " x ) )
32 eqss 
 |-  ( ( ( int ` J ) ` ( `' F " x ) ) = ( `' F " x ) <-> ( ( ( int ` J ) ` ( `' F " x ) ) C_ ( `' F " x ) /\ ( `' F " x ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) )
33 32 baib 
 |-  ( ( ( int ` J ) ` ( `' F " x ) ) C_ ( `' F " x ) -> ( ( ( int ` J ) ` ( `' F " x ) ) = ( `' F " x ) <-> ( `' F " x ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) )
34 31 33 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> ( ( ( int ` J ) ` ( `' F " x ) ) = ( `' F " x ) <-> ( `' F " x ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) )
35 29 isopn3 
 |-  ( ( J e. Top /\ ( `' F " x ) C_ U. J ) -> ( ( `' F " x ) e. J <-> ( ( int ` J ) ` ( `' F " x ) ) = ( `' F " x ) ) )
36 21 28 35 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> ( ( `' F " x ) e. J <-> ( ( int ` J ) ` ( `' F " x ) ) = ( `' F " x ) ) )
37 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
38 37 ad3antlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> K e. Top )
39 isopn3i 
 |-  ( ( K e. Top /\ x e. K ) -> ( ( int ` K ) ` x ) = x )
40 38 39 sylancom 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> ( ( int ` K ) ` x ) = x )
41 40 imaeq2d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> ( `' F " ( ( int ` K ) ` x ) ) = ( `' F " x ) )
42 41 sseq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> ( ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) <-> ( `' F " x ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) )
43 34 36 42 3bitr4rd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. K ) -> ( ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) <-> ( `' F " x ) e. J ) )
44 43 pm5.74da 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( x e. K -> ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) <-> ( x e. K -> ( `' F " x ) e. J ) ) )
45 19 44 sylibd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( x e. ~P Y -> ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) -> ( x e. K -> ( `' F " x ) e. J ) ) )
46 45 ralimdv2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. ~P Y ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) -> A. x e. K ( `' F " x ) e. J ) )
47 46 imdistanda 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. x e. ~P Y ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) -> ( F : X --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
48 iscn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
49 47 48 sylibrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. x e. ~P Y ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) -> F e. ( J Cn K ) ) )
50 13 49 impbid 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ~P Y ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) ) )