# 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 e. Conn -> K e. Conn ) )

### Proof

Step Hyp Ref Expression
1 hmph
|-  ( J ~= K <-> ( J Homeo K ) =/= (/) )
2 n0
|-  ( ( J Homeo K ) =/= (/) <-> E. f f e. ( J Homeo K ) )
3 eqid
|-  U. J = U. J
4 eqid
|-  U. K = U. K
5 3 4 hmeof1o
|-  ( f e. ( J Homeo K ) -> f : U. J -1-1-onto-> U. K )
6 f1ofo
|-  ( f : U. J -1-1-onto-> U. K -> f : U. J -onto-> U. K )
7 5 6 syl
|-  ( f e. ( J Homeo K ) -> f : U. J -onto-> U. K )
8 hmeocn
|-  ( f e. ( J Homeo K ) -> f e. ( J Cn K ) )
9 4 cnconn
|-  ( ( J e. Conn /\ f : U. J -onto-> U. K /\ f e. ( J Cn K ) ) -> K e. Conn )
10 9 3expb
|-  ( ( J e. Conn /\ ( f : U. J -onto-> U. K /\ f e. ( J Cn K ) ) ) -> K e. Conn )
11 10 expcom
|-  ( ( f : U. J -onto-> U. K /\ f e. ( J Cn K ) ) -> ( J e. Conn -> K e. Conn ) )
12 7 8 11 syl2anc
|-  ( f e. ( J Homeo K ) -> ( J e. Conn -> K e. Conn ) )
13 12 exlimiv
|-  ( E. f f e. ( J Homeo K ) -> ( J e. Conn -> K e. Conn ) )
14 2 13 sylbi
|-  ( ( J Homeo K ) =/= (/) -> ( J e. Conn -> K e. Conn ) )
15 1 14 sylbi
|-  ( J ~= K -> ( J e. Conn -> K e. Conn ) )