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

Metamath Proof Explorer

Theorem hmphen

Description: Homeomorphisms preserve the cardinality of the topologies. (Contributed by FL, 1-Jun-2008) (Revised by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion hmphen ⊢ J ≃ K → J ≈ K

Proof

Step Hyp Ref Expression
1 hmph ⊢ J ≃ K ↔ J Homeo K ≠ ∅
2 n0 ⊢ J Homeo K ≠ ∅ ↔ ∃ f f ∈ J Homeo K
3 hmeocn ⊢ f ∈ J Homeo K → f ∈ J Cn K
4 cntop1 ⊢ f ∈ J Cn K → J ∈ Top
5 3 4 syl ⊢ f ∈ J Homeo K → J ∈ Top
6 cntop2 ⊢ f ∈ J Cn K → K ∈ Top
7 3 6 syl ⊢ f ∈ J Homeo K → K ∈ Top
8 eqid ⊢ x ∈ J ⟼ f x = x ∈ J ⟼ f x
9 8 hmeoimaf1o ⊢ f ∈ J Homeo K → x ∈ J ⟼ f x : J ⟶ 1-1 onto K
10 f1oen2g ⊢ J ∈ Top ∧ K ∈ Top ∧ x ∈ J ⟼ f x : J ⟶ 1-1 onto K → J ≈ K
11 5 7 9 10 syl3anc ⊢ f ∈ J Homeo K → J ≈ K
12 11 exlimiv ⊢ ∃ f f ∈ J Homeo K → J ≈ K
13 2 12 sylbi ⊢ J Homeo K ≠ ∅ → J ≈ K
14 1 13 sylbi ⊢ J ≃ K → J ≈ K