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