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 = U. J
	cmphaushmeo.2	|- Y = U. K
Assertion	hmphen2	|- ( J ~= K -> X ~~ Y )

Proof

Step	Hyp	Ref	Expression
1		cmphaushmeo.1	|- X = U. J
2		cmphaushmeo.2	|- Y = U. K
3		hmph	|- ( J ~= K <-> ( J Homeo K ) =/= (/) )
4		n0	|- ( ( J Homeo K ) =/= (/) <-> E. f f e. ( J Homeo K ) )
5	1 2	hmeof1o	|- ( f e. ( J Homeo K ) -> f : X -1-1-onto-> Y )
6		f1oen3g	|- ( ( f e. ( J Homeo K ) /\ f : X -1-1-onto-> Y ) -> X ~~ Y )
7	5 6	mpdan	|- ( f e. ( J Homeo K ) -> X ~~ Y )
8	7	exlimiv	|- ( E. f f e. ( J Homeo K ) -> X ~~ Y )
9	4 8	sylbi	|- ( ( J Homeo K ) =/= (/) -> X ~~ Y )
10	3 9	sylbi	|- ( J ~= K -> X ~~ Y )