# Metamath Proof Explorer

## Theorem hmphen2

Description: Homeomorphisms preserve the cardinality of the underlying sets. (Contributed by FL, 17-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypotheses cmphaushmeo.1 ${⊢}{X}=\bigcup {J}$
cmphaushmeo.2 ${⊢}{Y}=\bigcup {K}$
Assertion hmphen2 ${⊢}{J}\simeq {K}\to {X}\approx {Y}$

### Proof

Step Hyp Ref Expression
1 cmphaushmeo.1 ${⊢}{X}=\bigcup {J}$
2 cmphaushmeo.2 ${⊢}{Y}=\bigcup {K}$
3 hmph ${⊢}{J}\simeq {K}↔{J}\mathrm{Homeo}{K}\ne \varnothing$
4 n0 ${⊢}{J}\mathrm{Homeo}{K}\ne \varnothing ↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({J}\mathrm{Homeo}{K}\right)$
5 1 2 hmeof1o ${⊢}{f}\in \left({J}\mathrm{Homeo}{K}\right)\to {f}:{X}\underset{1-1 onto}{⟶}{Y}$
6 f1oen3g ${⊢}\left({f}\in \left({J}\mathrm{Homeo}{K}\right)\wedge {f}:{X}\underset{1-1 onto}{⟶}{Y}\right)\to {X}\approx {Y}$
7 5 6 mpdan ${⊢}{f}\in \left({J}\mathrm{Homeo}{K}\right)\to {X}\approx {Y}$
8 7 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({J}\mathrm{Homeo}{K}\right)\to {X}\approx {Y}$
9 4 8 sylbi ${⊢}{J}\mathrm{Homeo}{K}\ne \varnothing \to {X}\approx {Y}$
10 3 9 sylbi ${⊢}{J}\simeq {K}\to {X}\approx {Y}$