This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-hmph

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

		Ref	Expression
	Assertion	df-hmph	$⊢ ≃ = {Homeo}^{-1} [V ∖ 1_{𝑜}]$

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