Theorem phtpy01

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

	Ref	Expression
Hypotheses	isphtpy.2	|- ( ph -> F e. ( II Cn J ) )
	isphtpy.3	|- ( ph -> G e. ( II Cn J ) )
	phtpyi.1	|- ( ph -> H e. ( F ( PHtpy ` J ) G ) )
Assertion	phtpy01	|- ( ph -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isphtpy.2	|- ( ph -> F e. ( II Cn J ) )
2		isphtpy.3	|- ( ph -> G e. ( II Cn J ) )
3		phtpyi.1	|- ( ph -> H e. ( F ( PHtpy ` J ) G ) )
4		1elunit	|- 1 e. ( 0 [,] 1 )
5	1 2 3	phtpyi	|- ( ( ph /\ 1 e. ( 0 [,] 1 ) ) -> ( ( 0 H 1 ) = ( F ` 0 ) /\ ( 1 H 1 ) = ( F ` 1 ) ) )
6	4 5	mpan2	|- ( ph -> ( ( 0 H 1 ) = ( F ` 0 ) /\ ( 1 H 1 ) = ( F ` 1 ) ) )
7	6	simpld	|- ( ph -> ( 0 H 1 ) = ( F ` 0 ) )
8		0elunit	|- 0 e. ( 0 [,] 1 )
9		iitopon	|- II e. ( TopOn ` ( 0 [,] 1 ) )
10	9	a1i	|- ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
11	1 2	phtpyhtpy	|- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( F ( II Htpy J ) G ) )
12	11 3	sseldd	|- ( ph -> H e. ( F ( II Htpy J ) G ) )
13	10 1 2 12	htpyi	|- ( ( ph /\ 0 e. ( 0 [,] 1 ) ) -> ( ( 0 H 0 ) = ( F ` 0 ) /\ ( 0 H 1 ) = ( G ` 0 ) ) )
14	8 13	mpan2	|- ( ph -> ( ( 0 H 0 ) = ( F ` 0 ) /\ ( 0 H 1 ) = ( G ` 0 ) ) )
15	14	simprd	|- ( ph -> ( 0 H 1 ) = ( G ` 0 ) )
16	7 15	eqtr3d	|- ( ph -> ( F ` 0 ) = ( G ` 0 ) )
17	6	simprd	|- ( ph -> ( 1 H 1 ) = ( F ` 1 ) )
18	10 1 2 12	htpyi	|- ( ( ph /\ 1 e. ( 0 [,] 1 ) ) -> ( ( 1 H 0 ) = ( F ` 1 ) /\ ( 1 H 1 ) = ( G ` 1 ) ) )
19	4 18	mpan2	|- ( ph -> ( ( 1 H 0 ) = ( F ` 1 ) /\ ( 1 H 1 ) = ( G ` 1 ) ) )
20	19	simprd	|- ( ph -> ( 1 H 1 ) = ( G ` 1 ) )
21	17 20	eqtr3d	|- ( ph -> ( F ` 1 ) = ( G ` 1 ) )
22	16 21	jca	|- ( ph -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )