Theorem 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	$$⊢\simeq \mathrm{Er}\mathrm{Top}$$

Proof

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