Metamath Proof Explorer

Theorem cncnp

Description: A continuous function is continuous at all points. Theorem 7.2(g) of Munkres p. 107. (Contributed by NM, 15-May-2007) (Proof shortened by Mario Carneiro, 21-Aug-2015)

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

Proof

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