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 | |- ( ph -> C e. ( *Met ` X ) ) |
||
| metcnp4.6 | |- ( ph -> D e. ( *Met ` Y ) ) |
||
| metcnp4.7 | |- ( ph -> P e. X ) |
||
| Assertion | metcnp4 | |- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) ) |
| 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 | metcnp4.7 | |- ( ph -> P e. X ) |
|
| 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 | 1stccnp | |- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) ) |