# 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 )`