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

Metamath Proof Explorer

Theorem connhmph

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

Ref Expression
Assertion connhmph ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Conn → 𝐾 ∈ Conn ) )

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 cnconn ⊢ ( ( 𝐽 ∈ Conn ∧ 𝑓 : ∪ 𝐽 –onto→ ∪ 𝐾 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Conn )
10 9 3expb ⊢ ( ( 𝐽 ∈ Conn ∧ ( 𝑓 : ∪ 𝐽 –onto→ ∪ 𝐾 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) ) → 𝐾 ∈ Conn )
11 10 expcom ⊢ ( ( 𝑓 : ∪ 𝐽 –onto→ ∪ 𝐾 ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐽 ∈ Conn → 𝐾 ∈ Conn ) )
12 7 8 11 syl2anc ⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → ( 𝐽 ∈ Conn → 𝐾 ∈ Conn ) )
13 12 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → ( 𝐽 ∈ Conn → 𝐾 ∈ Conn ) )
14 2 13 sylbi ⊢ ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ → ( 𝐽 ∈ Conn → 𝐾 ∈ Conn ) )
15 1 14 sylbi ⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Conn → 𝐾 ∈ Conn ) )