# Metamath Proof Explorer

## 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 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
isphtpy.3 ${⊢}{\phi }\to {G}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
phtpyi.1 ${⊢}{\phi }\to {H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)$
Assertion phtpy01 ${⊢}{\phi }\to \left({F}\left(0\right)={G}\left(0\right)\wedge {F}\left(1\right)={G}\left(1\right)\right)$

### Proof

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