# 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 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
isphtpy.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
isphtpyd.1 ( 𝜑𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
isphtpyd.2 ( ( 𝜑𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) )
isphtpyd.3 ( ( 𝜑𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) )
Assertion isphtpyd ( 𝜑𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )

### Proof

Step Hyp Ref Expression
1 isphtpy.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
2 isphtpy.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
3 isphtpyd.1 ( 𝜑𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
4 isphtpyd.2 ( ( 𝜑𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) )
5 isphtpyd.3 ( ( 𝜑𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) )
6 4 5 jca ( ( 𝜑𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) )
7 6 ralrimiva ( 𝜑 → ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) )
8 1 2 isphtpy ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ↔ ( 𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∧ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) ) )
9 3 7 8 mpbir2and ( 𝜑𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )