This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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