phtpc01

Description: Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015)

		Ref	Expression
	Assertion	phtpc01	$⊢ F ≃_{ph} (J) G \to (F (0) = G (0) \land F (1) = G (1))$

Step	Hyp	Ref	Expression
1		isphtpc	$⊢ F ≃_{ph} (J) G \leftrightarrow (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset)$
2		n0	$⊢ F PHtpy (J) G \neq \emptyset \leftrightarrow \exists h h \in (F PHtpy (J) G)$
3		simpll	$⊢ ((F \in (II Cn J) \land G \in (II Cn J)) \land h \in (F PHtpy (J) G)) \to F \in (II Cn J)$
4		simplr	$⊢ ((F \in (II Cn J) \land G \in (II Cn J)) \land h \in (F PHtpy (J) G)) \to G \in (II Cn J)$
5		simpr	$⊢ ((F \in (II Cn J) \land G \in (II Cn J)) \land h \in (F PHtpy (J) G)) \to h \in (F PHtpy (J) G)$
6	3 4 5	phtpy01	$⊢ ((F \in (II Cn J) \land G \in (II Cn J)) \land h \in (F PHtpy (J) G)) \to (F (0) = G (0) \land F (1) = G (1))$
7	6	ex	$⊢ (F \in (II Cn J) \land G \in (II Cn J)) \to (h \in (F PHtpy (J) G) \to (F (0) = G (0) \land F (1) = G (1)))$
8	7	exlimdv	$⊢ (F \in (II Cn J) \land G \in (II Cn J)) \to (\exists h h \in (F PHtpy (J) G) \to (F (0) = G (0) \land F (1) = G (1)))$
9	2 8	biimtrid	$⊢ (F \in (II Cn J) \land G \in (II Cn J)) \to (F PHtpy (J) G \neq \emptyset \to (F (0) = G (0) \land F (1) = G (1)))$
10	9	3impia	$⊢ (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset) \to (F (0) = G (0) \land F (1) = G (1))$
11	1 10	sylbi	$⊢ F ≃_{ph} (J) G \to (F (0) = G (0) \land F (1) = G (1))$

Metamath Proof Explorer