issconn

Description: The property of being a simply connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	issconn	$⊢ J \in SConn \leftrightarrow (J \in PConn \land \forall f \in (II Cn J) (f (0) = f (1) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\})))$

Step	Hyp	Ref	Expression
1		oveq2	$⊢ j = J \to II Cn j = II Cn J$
2		fveq2	$⊢ j = J \to ≃_{ph} (j) = ≃_{ph} (J)$
3	2	breqd	$⊢ j = J \to (f ≃_{ph} (j) ([0, 1] \times \{f (0)\}) \leftrightarrow f ≃_{ph} (J) ([0, 1] \times \{f (0)\}))$
4	3	imbi2d	$⊢ j = J \to ((f (0) = f (1) \to f ≃_{ph} (j) ([0, 1] \times \{f (0)\})) \leftrightarrow (f (0) = f (1) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\})))$
5	1 4	raleqbidv	$⊢ j = J \to (\forall f \in (II Cn j) (f (0) = f (1) \to f ≃_{ph} (j) ([0, 1] \times \{f (0)\})) \leftrightarrow \forall f \in (II Cn J) (f (0) = f (1) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\})))$
6		df-sconn	$⊢ SConn = \{j \in PConn \| \forall f \in (II Cn j) (f (0) = f (1) \to f ≃_{ph} (j) ([0, 1] \times \{f (0)\}))\}$
7	5 6	elrab2	$⊢ J \in SConn \leftrightarrow (J \in PConn \land \forall f \in (II Cn J) (f (0) = f (1) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\})))$

Metamath Proof Explorer