Definition df-hmph

Description: Definition of the relation x is homeomorphic to y . (Contributed by FL, 14-Feb-2007)

	Ref	Expression
Assertion	df-hmph	$$⊢\simeq ={\mathrm{Homeo}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chmph	$$class\simeq$$
1		chmeo	$$class\mathrm{Homeo}$$
2	1	ccnv	$$class{\mathrm{Homeo}}^{-1}$$
3		cvv	$$class\mathrm{V}$$
4		c1o	$$class{1}_{𝑜}$$
5	3 4	cdif	$$class\left(\mathrm{V}\setminus 1_{𝑜}\right)$$
6	2 5	cima	$$class{\mathrm{Homeo}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
7	0 6	wceq	$$wff\simeq ={\mathrm{Homeo}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$