Theorem hmphsym

Description: "Is homeomorphic to" is symmetric. (Contributed by FL, 8-Mar-2007) (Proof shortened by Mario Carneiro, 30-May-2014)

	Ref	Expression
Assertion	hmphsym	$$⊢J\simeq K\to K\simeq J$$

Proof

Step	Hyp	Ref	Expression
1		hmph	$$⊢J\simeq K\leftrightarrow J\mathrm{Homeo}K\ne \varnothing$$
2		n0	$$⊢J\mathrm{Homeo}K\ne \varnothing \leftrightarrow \exists ff\in \left(J\mathrm{Homeo}K\right)$$
3	1 2	bitri	$$⊢J\simeq K\leftrightarrow \exists ff\in \left(J\mathrm{Homeo}K\right)$$
4		hmeocnv	$$⊢f\in \left(J\mathrm{Homeo}K\right)\to f^{-1}\in \left(K\mathrm{Homeo}J\right)$$
5		hmphi	$$⊢f^{-1}\in \left(K\mathrm{Homeo}J\right)\to K\simeq J$$
6	4 5	syl	$$⊢f\in \left(J\mathrm{Homeo}K\right)\to K\simeq J$$
7	6	exlimiv	$$⊢\exists ff\in \left(J\mathrm{Homeo}K\right)\to K\simeq J$$
8	3 7	sylbi	$$⊢J\simeq K\to K\simeq J$$