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