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\simeq K\to J\approx K$$

Proof

Step	Hyp	Ref	Expression
1		hmph	$$⊢J\simeq K\leftrightarrow J\mathrm{Homeo}K\ne \varnothing$$
2		n0	$$⊢J\mathrm{Homeo}K\ne \varnothing \leftrightarrow \exists ff\in \left(J\mathrm{Homeo}K\right)$$
3		hmeocn	$$⊢f\in \left(J\mathrm{Homeo}K\right)\to f\in \left(J\mathrm{Cn}K\right)$$
4		cntop1	$$⊢f\in \left(J\mathrm{Cn}K\right)\to J\in \mathrm{Top}$$
5	3 4	syl	$$⊢f\in \left(J\mathrm{Homeo}K\right)\to J\in \mathrm{Top}$$
6		cntop2	$$⊢f\in \left(J\mathrm{Cn}K\right)\to K\in \mathrm{Top}$$
7	3 6	syl	$$⊢f\in \left(J\mathrm{Homeo}K\right)\to K\in \mathrm{Top}$$
8		eqid	$$⊢\left(x\in J⟼f\left[x\right]\right)=\left(x\in J⟼f\left[x\right]\right)$$
9	8	hmeoimaf1o	$$⊢f\in \left(J\mathrm{Homeo}K\right)\to \left(x\in J⟼f\left[x\right]\right):J\underset{1-1\; onto}{⟶}K$$
10		f1oen2g	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\wedge \left(x\in J⟼f\left[x\right]\right):J\underset{1-1\; onto}{⟶}K\right)\to J\approx K$$
11	5 7 9 10	syl3anc	$$⊢f\in \left(J\mathrm{Homeo}K\right)\to J\approx K$$
12	11	exlimiv	$$⊢\exists ff\in \left(J\mathrm{Homeo}K\right)\to J\approx K$$
13	2 12	sylbi	$$⊢J\mathrm{Homeo}K\ne \varnothing \to J\approx K$$
14	1 13	sylbi	$$⊢J\simeq K\to J\approx K$$