Theorem phtpc01

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

	Ref	Expression
Assertion	phtpc01	⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isphtpc	⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) )
2		n0	⊢ ( ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ↔ ∃ ℎ ℎ ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
3		simpll	⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ℎ ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → 𝐹 ∈ ( II Cn 𝐽 ) )
4		simplr	⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ℎ ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → 𝐺 ∈ ( II Cn 𝐽 ) )
5		simpr	⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ℎ ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → ℎ ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
6	3 4 5	phtpy01	⊢ ( ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ℎ ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ) → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )
7	6	ex	⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) → ( ℎ ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) ) )
8	7	exlimdv	⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) → ( ∃ ℎ ℎ ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) ) )
9	2 8	syl5bi	⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) → ( ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) ) )
10	9	3impia	⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ≠ ∅ ) → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )
11	1 10	sylbi	⊢ ( 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )