Metamath Proof Explorer

Theorem metcn4

Description: Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.3 of Munkres p. 128. (Contributed by NM, 13-Jun-2007) (Revised by Mario Carneiro, 4-May-2014)

Ref Expression
Hypotheses metcnp4.3 ⊢ J = MetOpen ⁡ C
metcnp4.4 ⊢ K = MetOpen ⁡ D
metcnp4.5 ⊢ φ → C ∈ ∞Met ⁡ X
metcnp4.6 ⊢ φ → D ∈ ∞Met ⁡ Y
metcn4.7 ⊢ φ → F : X ⟶ Y
Assertion metcn4 ⊢ φ → F ∈ J Cn K ↔ ∀ f f : ℕ ⟶ X → ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x

Proof

Step Hyp Ref Expression
1 metcnp4.3 ⊢ J = MetOpen ⁡ C
2 metcnp4.4 ⊢ K = MetOpen ⁡ D
3 metcnp4.5 ⊢ φ → C ∈ ∞Met ⁡ X
4 metcnp4.6 ⊢ φ → D ∈ ∞Met ⁡ Y
5 metcn4.7 ⊢ φ → F : X ⟶ Y
6 1 met1stc ⊢ C ∈ ∞Met ⁡ X → J ∈ 1 st 𝜔
7 3 6 syl ⊢ φ → J ∈ 1 st 𝜔
8 1 mopntopon ⊢ C ∈ ∞Met ⁡ X → J ∈ TopOn ⁡ X
9 3 8 syl ⊢ φ → J ∈ TopOn ⁡ X
10 2 mopntopon ⊢ D ∈ ∞Met ⁡ Y → K ∈ TopOn ⁡ Y
11 4 10 syl ⊢ φ → K ∈ TopOn ⁡ Y
12 7 9 11 5 1stccn ⊢ φ → F ∈ J Cn K ↔ ∀ f f : ℕ ⟶ X → ∀ x f ⇝t ⁡ J x → F ∘ f ⇝t ⁡ K F ⁡ x