Metamath Proof Explorer


Theorem cnptop1

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

Ref Expression
Assertion cnptop1
|- ( F e. ( ( J CnP K ) ` P ) -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid
 |-  U. J = 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. U. J ) /\ ( F : U. J --> 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. U. J ) )
5 4 simp1d
 |-  ( F e. ( ( J CnP K ) ` P ) -> J e. Top )