Metamath Proof Explorer

Theorem metcnp4

Description: Two ways to say a mapping from metric C to metric D is continuous at point P . Theorem 14-4.3 of Gleason p. 240. (Contributed by NM, 17-May-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
metcnp4.7 ⊢ φ → P ∈ X
Assertion metcnp4 ⊢ φ → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ f f : ℕ ⟶ X ∧ f ⇝t ⁡ J P → F ∘ f ⇝t ⁡ K F ⁡ P

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 metcnp4.7 ⊢ φ → P ∈ X
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 1stccnp ⊢ φ → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ f f : ℕ ⟶ X ∧ f ⇝t ⁡ J P → F ∘ f ⇝t ⁡ K F ⁡ P