Metamath Proof Explorer


Theorem hmphtop2

Description: The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion hmphtop2
|- ( J ~= K -> K e. Top )

Proof

Step Hyp Ref Expression
1 hmphtop
 |-  ( J ~= K -> ( J e. Top /\ K e. Top ) )
2 1 simprd
 |-  ( J ~= K -> K e. Top )