Metamath Proof Explorer

Theorem connhmph

Description: Connectedness is a topological property. (Contributed by Jeff Hankins, 3-Jul-2009)

Ref Expression
Assertion connhmph ⊢ J ≃ K → J ∈ Conn → K ∈ Conn

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 cnconn ⊢ J ∈ Conn ∧ f : ⋃ J ⟶ onto ⋃ K ∧ f ∈ J Cn K → K ∈ Conn
10 9 3expb ⊢ J ∈ Conn ∧ f : ⋃ J ⟶ onto ⋃ K ∧ f ∈ J Cn K → K ∈ Conn
11 10 expcom ⊢ f : ⋃ J ⟶ onto ⋃ K ∧ f ∈ J Cn K → J ∈ Conn → K ∈ Conn
12 7 8 11 syl2anc ⊢ f ∈ J Homeo K → J ∈ Conn → K ∈ Conn
13 12 exlimiv ⊢ ∃ f f ∈ J Homeo K → J ∈ Conn → K ∈ Conn
14 2 13 sylbi ⊢ J Homeo K ≠ ∅ → J ∈ Conn → K ∈ Conn
15 1 14 sylbi ⊢ J ≃ K → J ∈ Conn → K ∈ Conn