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