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