Theorem cnprcl2

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

	Ref	Expression
Assertion	cnprcl2	|- ( ( J e. ( TopOn ` X ) /\ F e. ( ( J CnP K ) ` P ) ) -> P e. X )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- U. J = U. J
2	1	cnprcl	|- ( F e. ( ( J CnP K ) ` P ) -> P e. U. J )
3	2	adantl	|- ( ( J e. ( TopOn ` X ) /\ F e. ( ( J CnP K ) ` P ) ) -> P e. U. J )
4		toponuni	|- ( J e. ( TopOn ` X ) -> X = U. J )
5	4	adantr	|- ( ( J e. ( TopOn ` X ) /\ F e. ( ( J CnP K ) ` P ) ) -> X = U. J )
6	3 5	eleqtrrd	|- ( ( J e. ( TopOn ` X ) /\ F e. ( ( J CnP K ) ` P ) ) -> P e. X )