# Metamath Proof Explorer

## Theorem cnptop2

Description: Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnptop2 ${⊢}{F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\to {K}\in \mathrm{Top}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\bigcup {J}=\bigcup {J}$
2 eqid ${⊢}\bigcup {K}=\bigcup {K}$
3 1 2 iscnp2 ${⊢}{F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)↔\left(\left({J}\in \mathrm{Top}\wedge {K}\in \mathrm{Top}\wedge {P}\in \bigcup {J}\right)\wedge \left({F}:\bigcup {J}⟶\bigcup {K}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\right)$
4 3 simplbi ${⊢}{F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\to \left({J}\in \mathrm{Top}\wedge {K}\in \mathrm{Top}\wedge {P}\in \bigcup {J}\right)$
5 4 simp2d ${⊢}{F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\to {K}\in \mathrm{Top}$