This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ Comp → K ∈ Comp

Proof

Step Hyp Ref Expression
1 hmph ⊢ J ≃ K ↔ J Homeo K ≠ ∅
2 n0 ⊢ J Homeo K ≠ ∅ ↔ ∃ f f ∈ J Homeo K
3 eqid ⊢ ⋃ J = ⋃ J
4 eqid ⊢ ⋃ K = ⋃ K
5 3 4 hmeof1o ⊢ f ∈ J Homeo K → f : ⋃ J ⟶ 1-1 onto ⋃ K
6 f1ofo ⊢ f : ⋃ J ⟶ 1-1 onto ⋃ K → f : ⋃ J ⟶ onto ⋃ K
7 5 6 syl ⊢ f ∈ J Homeo K → f : ⋃ J ⟶ onto ⋃ K
8 hmeocn ⊢ f ∈ J Homeo K → f ∈ J Cn K
9 4 cncmp ⊢ J ∈ Comp ∧ f : ⋃ J ⟶ onto ⋃ K ∧ f ∈ J Cn K → K ∈ Comp
10 9 3expb ⊢ J ∈ Comp ∧ f : ⋃ J ⟶ onto ⋃ K ∧ f ∈ J Cn K → K ∈ Comp
11 10 expcom ⊢ f : ⋃ J ⟶ onto ⋃ K ∧ f ∈ J Cn K → J ∈ Comp → K ∈ Comp
12 7 8 11 syl2anc ⊢ f ∈ J Homeo K → J ∈ Comp → K ∈ Comp
13 12 exlimiv ⊢ ∃ f f ∈ J Homeo K → J ∈ Comp → K ∈ Comp
14 2 13 sylbi ⊢ J Homeo K ≠ ∅ → J ∈ Comp → K ∈ Comp
15 1 14 sylbi ⊢ J ≃ K → J ∈ Comp → K ∈ Comp