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