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	⊢ ( 𝐽 ∈ Top → 𝐽 ≃ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		toptopon2	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
2		idhmeo	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( I ↾ ∪ 𝐽 ) ∈ ( 𝐽 Homeo 𝐽 ) )
3	1 2	sylbi	⊢ ( 𝐽 ∈ Top → ( I ↾ ∪ 𝐽 ) ∈ ( 𝐽 Homeo 𝐽 ) )
4		hmphi	⊢ ( ( I ↾ ∪ 𝐽 ) ∈ ( 𝐽 Homeo 𝐽 ) → 𝐽 ≃ 𝐽 )
5	3 4	syl	⊢ ( 𝐽 ∈ Top → 𝐽 ≃ 𝐽 )