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)\leftrightarrow \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\left(F\left(P\right)\in y\to \exists x\in J\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}$$