hmpher

Description: "Is homeomorphic to" is an equivalence relation. (Contributed by FL, 22-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	hmpher	$⊢ ≃ Er Top$

Step	Hyp	Ref	Expression
1		df-hmph	$⊢ ≃ = {Homeo}^{-1} [V ∖ 1_{𝑜}]$
2		cnvimass	$⊢ {Homeo}^{-1} [V ∖ 1_{𝑜}] \subseteq dom Homeo$
3		hmeofn	$⊢ Homeo Fn (Top \times Top)$
4	3	fndmi	$⊢ dom Homeo = Top \times Top$
5	2 4	sseqtri	$⊢ {Homeo}^{-1} [V ∖ 1_{𝑜}] \subseteq Top \times Top$
6	1 5	eqsstri	$⊢ ≃ \subseteq Top \times Top$
7		relxp	$⊢ Rel (Top \times Top)$
8		relss	$⊢ ≃ \subseteq Top \times Top \to (Rel (Top \times Top) \to Rel ≃)$
9	6 7 8	mp2	$⊢ Rel ≃$
10		hmphsym	$⊢ x ≃ y \to y ≃ x$
11		hmphtr	$⊢ (x ≃ y \land y ≃ z) \to x ≃ z$
12		hmphref	$⊢ x \in Top \to x ≃ x$
13		hmphtop1	$⊢ x ≃ x \to x \in Top$
14	12 13	impbii	$⊢ x \in Top \leftrightarrow x ≃ x$
15	9 10 11 14	iseri	$⊢ ≃ Er Top$

Metamath Proof Explorer