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 = 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 )