Metamath Proof Explorer

Theorem phtpc01

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

Ref Expression
Assertion phtpc01 ⊢ F ≃ ph ⁡ J G → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1

Proof

Step Hyp Ref Expression
1 isphtpc ⊢ F ≃ ph ⁡ J G ↔ F ∈ II Cn J ∧ G ∈ II Cn J ∧ F PHtpy ⁡ J G ≠ ∅
2 n0 ⊢ F PHtpy ⁡ J G ≠ ∅ ↔ ∃ h h ∈ F PHtpy ⁡ J G
3 simpll ⊢ F ∈ II Cn J ∧ G ∈ II Cn J ∧ h ∈ F PHtpy ⁡ J G → F ∈ II Cn J
4 simplr ⊢ F ∈ II Cn J ∧ G ∈ II Cn J ∧ h ∈ F PHtpy ⁡ J G → G ∈ II Cn J
5 simpr ⊢ F ∈ II Cn J ∧ G ∈ II Cn J ∧ h ∈ F PHtpy ⁡ J G → h ∈ F PHtpy ⁡ J G
6 3 4 5 phtpy01 ⊢ F ∈ II Cn J ∧ G ∈ II Cn J ∧ h ∈ F PHtpy ⁡ J G → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1
7 6 ex ⊢ F ∈ II Cn J ∧ G ∈ II Cn J → h ∈ F PHtpy ⁡ J G → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1
8 7 exlimdv ⊢ F ∈ II Cn J ∧ G ∈ II Cn J → ∃ h h ∈ F PHtpy ⁡ J G → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1
9 2 8 syl5bi ⊢ F ∈ II Cn J ∧ G ∈ II Cn J → F PHtpy ⁡ J G ≠ ∅ → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1
10 9 3impia ⊢ F ∈ II Cn J ∧ G ∈ II Cn J ∧ F PHtpy ⁡ J G ≠ ∅ → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1
11 1 10 sylbi ⊢ F ≃ ph ⁡ J G → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1