Metamath Proof Explorer

Theorem hmph

Description: Express the predicate J is homeomorphic to K . (Contributed by FL, 14-Feb-2007) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion hmph 
|- ( J ~= K <-> ( J Homeo K ) =/= (/) )

Proof

Step Hyp Ref Expression
1 df-hmph 
 |-  ~= = ( `' Homeo " ( _V \ 1o ) )
2 hmeofn 
 |-  Homeo Fn ( Top X. Top )
3 1 2 brwitnlem 
 |-  ( J ~= K <-> ( J Homeo K ) =/= (/) )