# Metamath Proof Explorer

## Theorem cmphmph

Description: Compactness is a topological property-that is, for any two homeomorphic topologies, either both are compact or neither is. (Contributed by Jeff Hankins, 30-Jun-2009) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion cmphmph
`|- ( J ~= K -> ( J e. Comp -> K e. Comp ) )`

### 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 eqid
` |-  U. J = U. J`
4 eqid
` |-  U. K = U. K`
5 3 4 hmeof1o
` |-  ( f e. ( J Homeo K ) -> f : U. J -1-1-onto-> U. K )`
6 f1ofo
` |-  ( f : U. J -1-1-onto-> U. K -> f : U. J -onto-> U. K )`
7 5 6 syl
` |-  ( f e. ( J Homeo K ) -> f : U. J -onto-> U. K )`
8 hmeocn
` |-  ( f e. ( J Homeo K ) -> f e. ( J Cn K ) )`
9 4 cncmp
` |-  ( ( J e. Comp /\ f : U. J -onto-> U. K /\ f e. ( J Cn K ) ) -> K e. Comp )`
10 9 3expb
` |-  ( ( J e. Comp /\ ( f : U. J -onto-> U. K /\ f e. ( J Cn K ) ) ) -> K e. Comp )`
11 10 expcom
` |-  ( ( f : U. J -onto-> U. K /\ f e. ( J Cn K ) ) -> ( J e. Comp -> K e. Comp ) )`
12 7 8 11 syl2anc
` |-  ( f e. ( J Homeo K ) -> ( J e. Comp -> K e. Comp ) )`
13 12 exlimiv
` |-  ( E. f f e. ( J Homeo K ) -> ( J e. Comp -> K e. Comp ) )`
14 2 13 sylbi
` |-  ( ( J Homeo K ) =/= (/) -> ( J e. Comp -> K e. Comp ) )`
15 1 14 sylbi
` |-  ( J ~= K -> ( J e. Comp -> K e. Comp ) )`