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