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 e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )
2 n0 
 |-  ( ( F ( PHtpy ` J ) G ) =/= (/) <-> E. h h e. ( F ( PHtpy ` J ) G ) )
3 simpll 
 |-  ( ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) /\ h e. ( F ( PHtpy ` J ) G ) ) -> F e. ( II Cn J ) )
4 simplr 
 |-  ( ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) /\ h e. ( F ( PHtpy ` J ) G ) ) -> G e. ( II Cn J ) )
5 simpr 
 |-  ( ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) /\ h e. ( F ( PHtpy ` J ) G ) ) -> h e. ( F ( PHtpy ` J ) G ) )
6 3 4 5 phtpy01 
 |-  ( ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) /\ h e. ( F ( PHtpy ` J ) G ) ) -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) )
7 6 ex 
 |-  ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) -> ( h e. ( F ( PHtpy ` J ) G ) -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) ) )
8 7 exlimdv 
 |-  ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) -> ( E. h h e. ( F ( PHtpy ` J ) G ) -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) ) )
9 2 8 syl5bi 
 |-  ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) -> ( ( F ( PHtpy ` J ) G ) =/= (/) -> ( ( F ` 0 ) = ( G ` 0 ) /\ ( F ` 1 ) = ( G ` 1 ) ) ) )
10 9 3impia 
 |-  ( ( F e. ( II Cn J ) /\ G e. ( 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 ) ) )