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 \to (J \in Comp \to K \in Comp)$

Proof

Step	Hyp	Ref	Expression
1		hmph	$⊢ J ≃ K \leftrightarrow J Homeo K \neq \emptyset$
2		n0	$⊢ J Homeo K \neq \emptyset \leftrightarrow \exists f f \in (J Homeo K)$
3		eqid	$⊢ ⋃ J = ⋃ J$
4		eqid	$⊢ ⋃ K = ⋃ K$
5	3 4	hmeof1o	$⊢ f \in (J Homeo K) \to f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K$
6		f1ofo	$⊢ f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K \to f : ⋃ J \underset{onto}{⟶} ⋃ K$
7	5 6	syl	$⊢ f \in (J Homeo K) \to f : ⋃ J \underset{onto}{⟶} ⋃ K$
8		hmeocn	$⊢ f \in (J Homeo K) \to f \in (J Cn K)$
9	4	cncmp	$⊢ (J \in Comp \land f : ⋃ J \underset{onto}{⟶} ⋃ K \land f \in (J Cn K)) \to K \in Comp$
10	9	3expb	$⊢ (J \in Comp \land (f : ⋃ J \underset{onto}{⟶} ⋃ K \land f \in (J Cn K))) \to K \in Comp$
11	10	expcom	$⊢ (f : ⋃ J \underset{onto}{⟶} ⋃ K \land f \in (J Cn K)) \to (J \in Comp \to K \in Comp)$
12	7 8 11	syl2anc	$⊢ f \in (J Homeo K) \to (J \in Comp \to K \in Comp)$
13	12	exlimiv	$⊢ \exists f f \in (J Homeo K) \to (J \in Comp \to K \in Comp)$
14	2 13	sylbi	$⊢ J Homeo K \neq \emptyset \to (J \in Comp \to K \in Comp)$
15	1 14	sylbi	$⊢ J ≃ K \to (J \in Comp \to K \in Comp)$