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 ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Comp → 𝐾 ∈ Comp ) )

Proof

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