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	⊢ ≃ Er Top

Proof

Step	Hyp	Ref	Expression
1		df-hmph	⊢ ≃ = ( ◡ Homeo “ ( V ∖ 1o ) )
2		cnvimass	⊢ ( ◡ Homeo “ ( V ∖ 1o ) ) ⊆ dom Homeo
3		hmeofn	⊢ Homeo Fn ( Top × Top )
4	3	fndmi	⊢ dom Homeo = ( Top × Top )
5	2 4	sseqtri	⊢ ( ◡ Homeo “ ( V ∖ 1o ) ) ⊆ ( Top × Top )
6	1 5	eqsstri	⊢ ≃ ⊆ ( Top × Top )
7		relxp	⊢ Rel ( Top × Top )
8		relss	⊢ ( ≃ ⊆ ( Top × Top ) → ( Rel ( Top × Top ) → Rel ≃ ) )
9	6 7 8	mp2	⊢ Rel ≃
10		hmphsym	⊢ ( 𝑥 ≃ 𝑦 → 𝑦 ≃ 𝑥 )
11		hmphtr	⊢ ( ( 𝑥 ≃ 𝑦 ∧ 𝑦 ≃ 𝑧 ) → 𝑥 ≃ 𝑧 )
12		hmphref	⊢ ( 𝑥 ∈ Top → 𝑥 ≃ 𝑥 )
13		hmphtop1	⊢ ( 𝑥 ≃ 𝑥 → 𝑥 ∈ Top )
14	12 13	impbii	⊢ ( 𝑥 ∈ Top ↔ 𝑥 ≃ 𝑥 )
15	9 10 11 14	iseri	⊢ ≃ Er Top