Metamath Proof Explorer

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 ~= K -> J ~~ K )

Proof

Step Hyp Ref Expression
1 hmph 
 |-  ( J ~= K <-> ( J Homeo K ) =/= (/) )
2 n0 
 |-  ( ( J Homeo K ) =/= (/) <-> E. f f e. ( J Homeo K ) )
3 hmeocn 
 |-  ( f e. ( J Homeo K ) -> f e. ( J Cn K ) )
4 cntop1 
 |-  ( f e. ( J Cn K ) -> J e. Top )
5 3 4 syl 
 |-  ( f e. ( J Homeo K ) -> J e. Top )
6 cntop2 
 |-  ( f e. ( J Cn K ) -> K e. Top )
7 3 6 syl 
 |-  ( f e. ( J Homeo K ) -> K e. Top )
8 eqid 
 |-  ( x e. J |-> ( f " x ) ) = ( x e. J |-> ( f " x ) )
9 8 hmeoimaf1o 
 |-  ( f e. ( J Homeo K ) -> ( x e. J |-> ( f " x ) ) : J -1-1-onto-> K )
10 f1oen2g 
 |-  ( ( J e. Top /\ K e. Top /\ ( x e. J |-> ( f " x ) ) : J -1-1-onto-> K ) -> J ~~ K )
11 5 7 9 10 syl3anc 
 |-  ( f e. ( J Homeo K ) -> J ~~ K )
12 11 exlimiv 
 |-  ( E. f f e. ( J Homeo K ) -> J ~~ K )
13 2 12 sylbi 
 |-  ( ( J Homeo K ) =/= (/) -> J ~~ K )
14 1 13 sylbi 
 |-  ( J ~= K -> J ~~ K )