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 TopOn X K TopOn Y F J Cn K F : X Y x X F J CnP K x

Proof

Step Hyp Ref Expression
1 iscn J TopOn X K TopOn Y F J Cn K F : X Y y K F -1 y J
2 1 simprbda J TopOn X K TopOn Y F J Cn K F : X Y
3 eqid J = J
4 3 cncnpi F J Cn K x J F J CnP K x
5 4 ralrimiva F J Cn K x J F J CnP K x
6 5 adantl J TopOn X K TopOn Y F J Cn K x J F J CnP K x
7 toponuni J TopOn X X = J
8 7 ad2antrr J TopOn X K TopOn Y F J Cn K X = J
9 6 8 raleqtrrdv J TopOn X K TopOn Y F J Cn K x X F J CnP K x
10 2 9 jca J TopOn X K TopOn Y F J Cn K F : X Y x X F J CnP K x
11 simprl J TopOn X K TopOn Y F : X Y x X F J CnP K x F : X Y
12 cnvimass F -1 y dom F
13 fdm F : X Y dom F = X
14 13 adantl J TopOn X K TopOn Y y K F : X Y dom F = X
15 12 14 sseqtrid J TopOn X K TopOn Y y K F : X Y F -1 y X
16 ssralv F -1 y X x X F J CnP K x x F -1 y F J CnP K x
17 15 16 syl J TopOn X K TopOn Y y K F : X Y x X F J CnP K x x F -1 y F J CnP K x
18 simprr J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x F J CnP K x
19 simpllr J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x y K
20 ffn F : X Y F Fn X
21 20 ad2antlr J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x F Fn X
22 simprl J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x x F -1 y
23 elpreima F Fn X x F -1 y x X F x y
24 23 simplbda F Fn X x F -1 y F x y
25 21 22 24 syl2anc J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x F x y
26 cnpimaex F J CnP K x y K F x y u J x u F u y
27 18 19 25 26 syl3anc J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J x u F u y
28 simpllr J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J F : X Y
29 28 ffund J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J Fun F
30 simp-4l J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x J TopOn X
31 toponss J TopOn X u J u X
32 30 31 sylan J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J u X
33 28 13 syl J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J dom F = X
34 32 33 sseqtrrd J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J u dom F
35 funimass3 Fun F u dom F F u y u F -1 y
36 29 34 35 syl2anc J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J F u y u F -1 y
37 36 anbi2d J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J x u F u y x u u F -1 y
38 37 rexbidva J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J x u F u y u J x u u F -1 y
39 27 38 mpbid J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J x u u F -1 y
40 39 expr J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x u J x u u F -1 y
41 40 ralimdva J TopOn X K TopOn Y y K F : X Y x F -1 y F J CnP K x x F -1 y u J x u u F -1 y
42 17 41 syld J TopOn X K TopOn Y y K F : X Y x X F J CnP K x x F -1 y u J x u u F -1 y
43 42 impr J TopOn X K TopOn Y y K F : X Y x X F J CnP K x x F -1 y u J x u u F -1 y
44 43 an32s J TopOn X K TopOn Y F : X Y x X F J CnP K x y K x F -1 y u J x u u F -1 y
45 topontop J TopOn X J Top
46 45 ad3antrrr J TopOn X K TopOn Y F : X Y x X F J CnP K x y K J Top
47 eltop2 J Top F -1 y J x F -1 y u J x u u F -1 y
48 46 47 syl J TopOn X K TopOn Y F : X Y x X F J CnP K x y K F -1 y J x F -1 y u J x u u F -1 y
49 44 48 mpbird J TopOn X K TopOn Y F : X Y x X F J CnP K x y K F -1 y J
50 49 ralrimiva J TopOn X K TopOn Y F : X Y x X F J CnP K x y K F -1 y J
51 1 adantr J TopOn X K TopOn Y F : X Y x X F J CnP K x F J Cn K F : X Y y K F -1 y J
52 11 50 51 mpbir2and J TopOn X K TopOn Y F : X Y x X F J CnP K x F J Cn K
53 10 52 impbida J TopOn X K TopOn Y F J Cn K F : X Y x X F J CnP K x