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 ⊢ φ → F ∈ II Cn J
isphtpy.3 ⊢ φ → G ∈ II Cn J
phtpyi.1 ⊢ φ → H ∈ F PHtpy ⁡ J G
Assertion phtpy01 ⊢ φ → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢ φ → F ∈ II Cn J
2 isphtpy.3 ⊢ φ → G ∈ II Cn J
3 phtpyi.1 ⊢ φ → H ∈ F PHtpy ⁡ J G
4 1elunit ⊢ 1 ∈ 0 1
5 1 2 3 phtpyi ⊢ φ ∧ 1 ∈ 0 1 → 0 H 1 = F ⁡ 0 ∧ 1 H 1 = F ⁡ 1
6 4 5 mpan2 ⊢ φ → 0 H 1 = F ⁡ 0 ∧ 1 H 1 = F ⁡ 1
7 6 simpld ⊢ φ → 0 H 1 = F ⁡ 0
8 0elunit ⊢ 0 ∈ 0 1
9 iitopon ⊢ II ∈ TopOn ⁡ 0 1
10 9 a1i ⊢ φ → II ∈ TopOn ⁡ 0 1
11 1 2 phtpyhtpy ⊢ φ → F PHtpy ⁡ J G ⊆ F II Htpy J G
12 11 3 sseldd ⊢ φ → H ∈ F II Htpy J G
13 10 1 2 12 htpyi ⊢ φ ∧ 0 ∈ 0 1 → 0 H 0 = F ⁡ 0 ∧ 0 H 1 = G ⁡ 0
14 8 13 mpan2 ⊢ φ → 0 H 0 = F ⁡ 0 ∧ 0 H 1 = G ⁡ 0
15 14 simprd ⊢ φ → 0 H 1 = G ⁡ 0
16 7 15 eqtr3d ⊢ φ → F ⁡ 0 = G ⁡ 0
17 6 simprd ⊢ φ → 1 H 1 = F ⁡ 1
18 10 1 2 12 htpyi ⊢ φ ∧ 1 ∈ 0 1 → 1 H 0 = F ⁡ 1 ∧ 1 H 1 = G ⁡ 1
19 4 18 mpan2 ⊢ φ → 1 H 0 = F ⁡ 1 ∧ 1 H 1 = G ⁡ 1
20 19 simprd ⊢ φ → 1 H 1 = G ⁡ 1
21 17 20 eqtr3d ⊢ φ → F ⁡ 1 = G ⁡ 1
22 16 21 jca ⊢ φ → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1