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

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 = ⋃ J$
		cmphaushmeo.2	$⊢ Y = ⋃ K$
	Assertion	hmphen2	$⊢ J ≃ K \to X \approx Y$

Proof

Step	Hyp	Ref	Expression
1		cmphaushmeo.1	$⊢ X = ⋃ J$
2		cmphaushmeo.2	$⊢ Y = ⋃ K$
3		hmph	$⊢ J ≃ K \leftrightarrow J Homeo K \neq \emptyset$
4		n0	$⊢ J Homeo K \neq \emptyset \leftrightarrow \exists f f \in (J Homeo K)$
5	1 2	hmeof1o	$⊢ f \in (J Homeo K) \to f : X \underset{1-1 onto}{⟶} Y$
6		f1oen3g	$⊢ (f \in (J Homeo K) \land f : X \underset{1-1 onto}{⟶} Y) \to X \approx Y$
7	5 6	mpdan	$⊢ f \in (J Homeo K) \to X \approx Y$
8	7	exlimiv	$⊢ \exists f f \in (J Homeo K) \to X \approx Y$
9	4 8	sylbi	$⊢ J Homeo K \neq \emptyset \to X \approx Y$
10	3 9	sylbi	$⊢ J ≃ K \to X \approx Y$