Metamath Proof Explorer

Theorem isphtpy2d

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 𝐽 ) )
isphtpy2d.1 ⊢ ( 𝜑 → 𝐻 ∈ ( ( II ×t II ) Cn 𝐽 ) )
isphtpy2d.2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) )
isphtpy2d.3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) )
isphtpy2d.4 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) )
isphtpy2d.5 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) )
Assertion isphtpy2d ( 𝜑 → 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
2 isphtpy.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
3 isphtpy2d.1 ⊢ ( 𝜑 → 𝐻 ∈ ( ( II ×t II ) Cn 𝐽 ) )
4 isphtpy2d.2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) )
5 isphtpy2d.3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) )
6 isphtpy2d.4 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) )
7 isphtpy2d.5 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) )
8 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
9 8 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
10 9 1 2 3 4 5 ishtpyd ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
11 1 2 10 6 7 isphtpyd ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )