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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) )

Proof

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