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 = U. J
Assertion	cnprcl	|- ( F e. ( ( J CnP K ) ` P ) -> P e. X )

Proof

Step	Hyp	Ref	Expression
1		iscnp2.1	|- X = U. J
2		eqid	|- U. K = U. K
3	1 2	iscnp2	|- ( F e. ( ( J CnP K ) ` P ) <-> ( ( J e. Top /\ K e. Top /\ P e. X ) /\ ( F : X --> U. K /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
4	3	simplbi	|- ( F e. ( ( J CnP K ) ` P ) -> ( J e. Top /\ K e. Top /\ P e. X ) )
5	4	simp3d	|- ( F e. ( ( J CnP K ) ` P ) -> P e. X )