sconnpht

Description: A closed path in a simply connected space is contractible to a point. (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	sconnpht	$⊢ (J \in SConn \land F \in (II Cn J) \land F (0) = F (1)) \to F ≃_{ph} (J) ([0, 1] \times \{F (0)\})$

Step	Hyp	Ref	Expression
1		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)\})))$
2		fveq1	$⊢ f = F \to f (0) = F (0)$
3		fveq1	$⊢ f = F \to f (1) = F (1)$
4	2 3	eqeq12d	$⊢ f = F \to (f (0) = f (1) \leftrightarrow F (0) = F (1))$
5		id	$⊢ f = F \to f = F$
6	2	sneqd	$⊢ f = F \to \{f (0)\} = \{F (0)\}$
7	6	xpeq2d	$⊢ f = F \to [0, 1] \times \{f (0)\} = [0, 1] \times \{F (0)\}$
8	5 7	breq12d	$⊢ f = F \to (f ≃_{ph} (J) ([0, 1] \times \{f (0)\}) \leftrightarrow F ≃_{ph} (J) ([0, 1] \times \{F (0)\}))$
9	4 8	imbi12d	$⊢ f = F \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)\})))$
10	9	rspccv	$⊢ \forall f \in (II Cn J) (f (0) = f (1) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\})) \to (F \in (II Cn J) \to (F (0) = F (1) \to F ≃_{ph} (J) ([0, 1] \times \{F (0)\})))$
11	1 10	simplbiim	$⊢ J \in SConn \to (F \in (II Cn J) \to (F (0) = F (1) \to F ≃_{ph} (J) ([0, 1] \times \{F (0)\})))$
12	11	3imp	$⊢ (J \in SConn \land F \in (II Cn J) \land F (0) = F (1)) \to F ≃_{ph} (J) ([0, 1] \times \{F (0)\})$

Metamath Proof Explorer