Metamath Proof Explorer

Theorem metcn

Description: Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.1 of Munkres p. 127. The second biconditional argument says that for every positive "epsilon" y there is a positive "delta" z such that a distance less than delta in C maps to a distance less than epsilon in D . (Contributed by NM, 15-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses metcn.2 ⊢ J = MetOpen ⁡ C
metcn.4 ⊢ K = MetOpen ⁡ D
Assertion metcn ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ X ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ X x C w < z → F ⁡ x D F ⁡ w < y

Proof

Step Hyp Ref Expression
1 metcn.2 ⊢ J = MetOpen ⁡ C
2 metcn.4 ⊢ K = MetOpen ⁡ D
3 1 mopntopon ⊢ C ∈ ∞Met ⁡ X → J ∈ TopOn ⁡ X
4 2 mopntopon ⊢ D ∈ ∞Met ⁡ Y → K ∈ TopOn ⁡ Y
5 cncnp ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x
6 3 4 5 syl2an ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x
7 simplr ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ X → F : X ⟶ Y
8 1 2 metcnp ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ Y ∧ x ∈ X → F ∈ J CnP K ⁡ x ↔ F : X ⟶ Y ∧ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ X x C w < z → F ⁡ x D F ⁡ w < y
9 8 ad4ant124 ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ X → F ∈ J CnP K ⁡ x ↔ F : X ⟶ Y ∧ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ X x C w < z → F ⁡ x D F ⁡ w < y
10 7 9 mpbirand ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ X → F ∈ J CnP K ⁡ x ↔ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ X x C w < z → F ⁡ x D F ⁡ w < y
11 10 ralbidva ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ Y ∧ F : X ⟶ Y → ∀ x ∈ X F ∈ J CnP K ⁡ x ↔ ∀ x ∈ X ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ X x C w < z → F ⁡ x D F ⁡ w < y
12 11 pm5.32da ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ Y → F : X ⟶ Y ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x ↔ F : X ⟶ Y ∧ ∀ x ∈ X ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ X x C w < z → F ⁡ x D F ⁡ w < y
13 6 12 bitrd ⊢ C ∈ ∞Met ⁡ X ∧ D ∈ ∞Met ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ X ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ X x C w < z → F ⁡ x D F ⁡ w < y