Theorem cnprcl

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

	Ref	Expression
Hypothesis	iscnp2.1	$$⊢X=\bigcup J$$
Assertion	cnprcl	$$⊢F\in \left(J\mathrm{CnP}K\right)\left(P\right)\to P\in X$$

Proof

Step	Hyp	Ref	Expression
1		iscnp2.1	$$⊢X=\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 X\right)\wedge \left(F:X⟶\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 X\right)$$
5	4	simp3d	$$⊢F\in \left(J\mathrm{CnP}K\right)\left(P\right)\to P\in X$$