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 | |- ( ph -> C e. ( *Met ` X ) ) |
||
| metcnp4.6 | |- ( ph -> D e. ( *Met ` Y ) ) |
||
| metcn4.7 | |- ( ph -> F : X --> Y ) |
||
| Assertion | metcn4 | |- ( ph -> ( F e. ( J Cn K ) <-> A. f ( f : NN --> X -> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | metcnp4.3 | |- J = ( MetOpen ` C ) |
|
| 2 | metcnp4.4 | |- K = ( MetOpen ` D ) |
|
| 3 | metcnp4.5 | |- ( ph -> C e. ( *Met ` X ) ) |
|
| 4 | metcnp4.6 | |- ( ph -> D e. ( *Met ` Y ) ) |
|
| 5 | metcn4.7 | |- ( ph -> F : X --> Y ) |
|
| 6 | 1 | met1stc | |- ( C e. ( *Met ` X ) -> J e. 1stc ) |
| 7 | 3 6 | syl | |- ( ph -> J e. 1stc ) |
| 8 | 1 | mopntopon | |- ( C e. ( *Met ` X ) -> J e. ( TopOn ` X ) ) |
| 9 | 3 8 | syl | |- ( ph -> J e. ( TopOn ` X ) ) |
| 10 | 2 | mopntopon | |- ( D e. ( *Met ` Y ) -> K e. ( TopOn ` Y ) ) |
| 11 | 4 10 | syl | |- ( ph -> K e. ( TopOn ` Y ) ) |
| 12 | 7 9 11 5 | 1stccn | |- ( ph -> ( F e. ( J Cn K ) <-> A. f ( f : NN --> X -> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) ) ) |