phtpy01

Description: Two path-homotopic paths have the same start and end point. (Contributed by Mario Carneiro, 23-Feb-2015)

Step	Hyp	Ref	Expression
1		isphtpy.2	$⊢ φ \to F \in (II Cn J)$
2		isphtpy.3	$⊢ φ \to G \in (II Cn J)$
3		phtpyi.1	$⊢ φ \to H \in (F PHtpy (J) G)$
4		1elunit	$⊢ 1 \in [0, 1]$
5	1 2 3	phtpyi	$⊢ (φ \land 1 \in [0, 1]) \to (0 H 1 = F (0) \land 1 H 1 = F (1))$
6	4 5	mpan2	$⊢ φ \to (0 H 1 = F (0) \land 1 H 1 = F (1))$
7	6	simpld	$⊢ φ \to 0 H 1 = F (0)$
8		0elunit	$⊢ 0 \in [0, 1]$
9		iitopon	$⊢ II \in TopOn ([0, 1])$
10	9	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
11	1 2	phtpyhtpy	$⊢ φ \to F PHtpy (J) G \subseteq F (II Htpy J) G$
12	11 3	sseldd	$⊢ φ \to H \in (F (II Htpy J) G)$
13	10 1 2 12	htpyi	$⊢ (φ \land 0 \in [0, 1]) \to (0 H 0 = F (0) \land 0 H 1 = G (0))$
14	8 13	mpan2	$⊢ φ \to (0 H 0 = F (0) \land 0 H 1 = G (0))$
15	14	simprd	$⊢ φ \to 0 H 1 = G (0)$
16	7 15	eqtr3d	$⊢ φ \to F (0) = G (0)$
17	6	simprd	$⊢ φ \to 1 H 1 = F (1)$
18	10 1 2 12	htpyi	$⊢ (φ \land 1 \in [0, 1]) \to (1 H 0 = F (1) \land 1 H 1 = G (1))$
19	4 18	mpan2	$⊢ φ \to (1 H 0 = F (1) \land 1 H 1 = G (1))$
20	19	simprd	$⊢ φ \to 1 H 1 = G (1)$
21	17 20	eqtr3d	$⊢ φ \to F (1) = G (1)$
22	16 21	jca	$⊢ φ \to (F (0) = G (0) \land F (1) = G (1))$

Metamath Proof Explorer