connhmph

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

		Ref	Expression
	Assertion	connhmph	$⊢ J ≃ K \to (J \in Conn \to K \in Conn)$

Step	Hyp	Ref	Expression
1		hmph	$⊢ J ≃ K \leftrightarrow J Homeo K \neq \emptyset$
2		n0	$⊢ J Homeo K \neq \emptyset \leftrightarrow \exists f f \in (J Homeo K)$
3		eqid	$⊢ ⋃ J = ⋃ J$
4		eqid	$⊢ ⋃ K = ⋃ K$
5	3 4	hmeof1o	$⊢ f \in (J Homeo K) \to f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K$
6		f1ofo	$⊢ f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K \to f : ⋃ J \underset{onto}{⟶} ⋃ K$
7	5 6	syl	$⊢ f \in (J Homeo K) \to f : ⋃ J \underset{onto}{⟶} ⋃ K$
8		hmeocn	$⊢ f \in (J Homeo K) \to f \in (J Cn K)$
9	4	cnconn	$⊢ (J \in Conn \land f : ⋃ J \underset{onto}{⟶} ⋃ K \land f \in (J Cn K)) \to K \in Conn$
10	9	3expb	$⊢ (J \in Conn \land (f : ⋃ J \underset{onto}{⟶} ⋃ K \land f \in (J Cn K))) \to K \in Conn$
11	10	expcom	$⊢ (f : ⋃ J \underset{onto}{⟶} ⋃ K \land f \in (J Cn K)) \to (J \in Conn \to K \in Conn)$
12	7 8 11	syl2anc	$⊢ f \in (J Homeo K) \to (J \in Conn \to K \in Conn)$
13	12	exlimiv	$⊢ \exists f f \in (J Homeo K) \to (J \in Conn \to K \in Conn)$
14	2 13	sylbi	$⊢ J Homeo K \neq \emptyset \to (J \in Conn \to K \in Conn)$
15	1 14	sylbi	$⊢ J ≃ K \to (J \in Conn \to K \in Conn)$

Metamath Proof Explorer