# Metamath Proof Explorer

## Theorem isphtpyd

Description: Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses isphtpy.2
`|- ( ph -> F e. ( II Cn J ) )`
isphtpy.3
`|- ( ph -> G e. ( II Cn J ) )`
isphtpyd.1
`|- ( ph -> H e. ( F ( II Htpy J ) G ) )`
isphtpyd.2
`|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` 0 ) )`
isphtpyd.3
`|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` 1 ) )`
Assertion isphtpyd
`|- ( ph -> H e. ( F ( PHtpy ` J ) G ) )`

### Proof

Step Hyp Ref Expression
1 isphtpy.2
` |-  ( ph -> F e. ( II Cn J ) )`
2 isphtpy.3
` |-  ( ph -> G e. ( II Cn J ) )`
3 isphtpyd.1
` |-  ( ph -> H e. ( F ( II Htpy J ) G ) )`
4 isphtpyd.2
` |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` 0 ) )`
5 isphtpyd.3
` |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` 1 ) )`
6 4 5 jca
` |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) )`
7 6 ralrimiva
` |-  ( ph -> A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) )`
8 1 2 isphtpy
` |-  ( ph -> ( H e. ( F ( PHtpy ` J ) G ) <-> ( H e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) ) )`
9 3 7 8 mpbir2and
` |-  ( ph -> H e. ( F ( PHtpy ` J ) G ) )`