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 6 8 raleqtrrdv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> A. x e. X F e. ( ( J CnP K ) ` x ) )
10 2 9 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 ) ) )
11 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 )
12 cnvimass 
 |-  ( `' F " y ) C_ dom F
13 fdm 
 |-  ( F : X --> Y -> dom F = X )
14 13 adantl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) -> dom F = X )
15 12 14 sseqtrid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ y e. K ) /\ F : X --> Y ) -> ( `' F " y ) C_ X )
16 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 ) ) )
17 15 16 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 ) ) )
18 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 ) )
19 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 )
20 ffn 
 |-  ( F : X --> Y -> F Fn X )
21 20 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 )
22 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 ) )
23 elpreima 
 |-  ( F Fn X -> ( x e. ( `' F " y ) <-> ( x e. X /\ ( F ` x ) e. y ) ) )
24 23 simplbda 
 |-  ( ( F Fn X /\ x e. ( `' F " y ) ) -> ( F ` x ) e. y )
25 21 22 24 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 )
26 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 ) )
27 18 19 25 26 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 ) )
28 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 )
29 28 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 )
30 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 ) )
31 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ u e. J ) -> u C_ X )
32 30 31 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 )
33 28 13 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 )
34 32 33 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 )
35 funimass3 
 |-  ( ( Fun F /\ u C_ dom F ) -> ( ( F " u ) C_ y <-> u C_ ( `' F " y ) ) )
36 29 34 35 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 ) ) )
37 36 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 ) ) ) )
38 37 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 ) ) ) )
39 27 38 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 ) ) )
40 39 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 ) ) ) )
41 40 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 ) ) ) )
42 17 41 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 ) ) ) )
43 42 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 ) ) )
44 43 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 ) ) )
45 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
46 45 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 )
47 eltop2 
 |-  ( J e. Top -> ( ( `' F " y ) e. J <-> A. x e. ( `' F " y ) E. u e. J ( x e. u /\ u C_ ( `' F " y ) ) ) )
48 46 47 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 ) ) ) )
49 44 48 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 )
50 49 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 )
51 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 ) ) )
52 11 50 51 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 ) )
53 10 52 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 ) ) ) )