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