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 ⊢ X = ⋃ J
cncnp.2 ⊢ Y = ⋃ K
Assertion cncnp2 ⊢ X ≠ ∅ → F ∈ J Cn K ↔ ∀ x ∈ X F ∈ J CnP K ⁡ x

Proof

Step Hyp Ref Expression
1 cncnp.1 ⊢ X = ⋃ J
2 cncnp.2 ⊢ Y = ⋃ K
3 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
4 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
5 3 4 sylib ⊢ F ∈ J Cn K → J ∈ TopOn ⁡ X
6 cntop2 ⊢ F ∈ J Cn K → K ∈ Top
7 2 toptopon ⊢ K ∈ Top ↔ K ∈ TopOn ⁡ Y
8 6 7 sylib ⊢ F ∈ J Cn K → K ∈ TopOn ⁡ Y
9 1 2 cnf ⊢ F ∈ J Cn K → F : X ⟶ Y
10 5 8 9 jca31 ⊢ F ∈ J Cn K → J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y
11 10 adantl ⊢ X ≠ ∅ ∧ F ∈ J Cn K → J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y
12 r19.2z ⊢ X ≠ ∅ ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x → ∃ x ∈ X F ∈ J CnP K ⁡ x
13 cnptop1 ⊢ F ∈ J CnP K ⁡ x → J ∈ Top
14 13 4 sylib ⊢ F ∈ J CnP K ⁡ x → J ∈ TopOn ⁡ X
15 cnptop2 ⊢ F ∈ J CnP K ⁡ x → K ∈ Top
16 15 7 sylib ⊢ F ∈ J CnP K ⁡ x → K ∈ TopOn ⁡ Y
17 1 2 cnpf ⊢ F ∈ J CnP K ⁡ x → F : X ⟶ Y
18 14 16 17 jca31 ⊢ F ∈ J CnP K ⁡ x → J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y
19 18 rexlimivw ⊢ ∃ x ∈ X F ∈ J CnP K ⁡ x → J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y
20 12 19 syl ⊢ X ≠ ∅ ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x → J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y
21 cncnp ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x
22 21 baibd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → F ∈ J Cn K ↔ ∀ x ∈ X F ∈ J CnP K ⁡ x
23 11 20 22 pm5.21nd ⊢ X ≠ ∅ → F ∈ J Cn K ↔ ∀ x ∈ X F ∈ J CnP K ⁡ x