Metamath Proof Explorer


Theorem cncnp2

Description: A continuous function is continuous at all points. Theorem 7.2(g) of Munkres p. 107. (Contributed by Raph Levien, 20-Nov-2006) (Proof shortened by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses cncnp.1 𝑋 = 𝐽
cncnp.2 𝑌 = 𝐾
Assertion cncnp2 ( 𝑋 ≠ ∅ → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 cncnp.1 𝑋 = 𝐽
2 cncnp.2 𝑌 = 𝐾
3 cntop1 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
4 1 toptopon ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 3 4 sylib ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 cntop2 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
7 2 toptopon ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
8 6 7 sylib ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
9 1 2 cnf ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋𝑌 )
10 5 8 9 jca31 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) )
11 10 adantl ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) )
12 r19.2z ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) → ∃ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) )
13 cnptop1 ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐽 ∈ Top )
14 13 4 sylib ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 cnptop2 ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐾 ∈ Top )
16 15 7 sylib ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
17 1 2 cnpf ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → 𝐹 : 𝑋𝑌 )
18 14 16 17 jca31 ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) )
19 18 rexlimivw ( ∃ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) )
20 12 19 syl ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) → ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) )
21 cncnp ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) )
22 21 baibd ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) )
23 11 20 22 pm5.21nd ( 𝑋 ≠ ∅ → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) )