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