Metamath Proof Explorer

Theorem cntop2

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

Ref Expression
Assertion cntop2 
|- ( F e. ( J Cn K ) -> K 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 simprd 
 |-  ( F e. ( J Cn K ) -> K e. Top )