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\leftrightarrow J\mathrm{Homeo}K\ne \varnothing$$
4		n0	$$⊢J\mathrm{Homeo}K\ne \varnothing \leftrightarrow \exists ff\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 ff\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$$