Metamath Proof Explorer


Theorem cntop1

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

Ref Expression
Assertion cntop1
|- ( F e. ( J Cn K ) -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid
 |-  U. J = U. J
2 eqid
 |-  U. K = U. K
3 1 2 iscn2
 |-  ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : U. J --> U. K /\ A. x e. K ( `' F " x ) e. J ) ) )
4 3 simplbi
 |-  ( F e. ( J Cn K ) -> ( J e. Top /\ K e. Top ) )
5 4 simpld
 |-  ( F e. ( J Cn K ) -> J e. Top )