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\simeq K\leftrightarrow J\mathrm{Homeo}K\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-hmph	$$⊢\simeq ={\mathrm{Homeo}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		hmeofn	$$⊢\mathrm{Homeo}Fn\left(\mathrm{Top}\times \mathrm{Top}\right)$$
3	1 2	brwitnlem	$$⊢J\simeq K\leftrightarrow J\mathrm{Homeo}K\ne \varnothing$$