Theorem hmphref

Description: "Is homeomorphic to" is reflexive. (Contributed by FL, 25-Feb-2007) (Proof shortened by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Assertion	hmphref	$$⊢J\in \mathrm{Top}\to J\simeq J$$

Proof

Step	Hyp	Ref	Expression
1		toptopon2	$$⊢J\in \mathrm{Top}\leftrightarrow J\in \mathrm{TopOn}\left(\bigcup J\right)$$
2		idhmeo	$$⊢J\in \mathrm{TopOn}\left(\bigcup J\right)\to {\mathrm{I}\upharpoonright }_{\bigcup J}\in \left(J\mathrm{Homeo}J\right)$$
3	1 2	sylbi	$$⊢J\in \mathrm{Top}\to {\mathrm{I}\upharpoonright }_{\bigcup J}\in \left(J\mathrm{Homeo}J\right)$$
4		hmphi	$$⊢{\mathrm{I}\upharpoonright }_{\bigcup J}\in \left(J\mathrm{Homeo}J\right)\to J\simeq J$$
5	3 4	syl	$$⊢J\in \mathrm{Top}\to J\simeq J$$