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 ( 𝐽 ≃ 𝐾 → 𝐽 ≈ 𝐾 )

Proof

Step Hyp Ref Expression
1 hmph ⊢ ( 𝐽 ≃ 𝐾 ↔ ( 𝐽 Homeo 𝐾 ) ≠ ∅ )
2 n0 ⊢ ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) )
3 hmeocn ⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
4 cntop1 ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
5 3 4 syl ⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐽 ∈ Top )
6 cntop2 ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
7 3 6 syl ⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐾 ∈ Top )
8 eqid ⊢ ( 𝑥 ∈ 𝐽 ↦ ( 𝑓 “ 𝑥 ) ) = ( 𝑥 ∈ 𝐽 ↦ ( 𝑓 “ 𝑥 ) )
9 8 hmeoimaf1o ⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → ( 𝑥 ∈ 𝐽 ↦ ( 𝑓 “ 𝑥 ) ) : 𝐽 –1-1-onto→ 𝐾 )
10 f1oen2g ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ↦ ( 𝑓 “ 𝑥 ) ) : 𝐽 –1-1-onto→ 𝐾 ) → 𝐽 ≈ 𝐾 )
11 5 7 9 10 syl3anc ⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐽 ≈ 𝐾 )
12 11 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐽 ≈ 𝐾 )
13 2 12 sylbi ⊢ ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ → 𝐽 ≈ 𝐾 )
14 1 13 sylbi ⊢ ( 𝐽 ≃ 𝐾 → 𝐽 ≈ 𝐾 )