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 ⊢φ→F∈IICnJ
isphtpy.3 ⊢φ→G∈IICnJ
isphtpy2d.1 ⊢φ→H∈II×tIICnJ
isphtpy2d.2 ⊢φ∧s∈01→sH0=F⁡s
isphtpy2d.3 ⊢φ∧s∈01→sH1=G⁡s
isphtpy2d.4 ⊢φ∧s∈01→0Hs=F⁡0
isphtpy2d.5 ⊢φ∧s∈01→1Hs=F⁡1
Assertion isphtpy2d ⊢φ→H∈FPHtpy⁡JG

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢φ→F∈IICnJ
2 isphtpy.3 ⊢φ→G∈IICnJ
3 isphtpy2d.1 ⊢φ→H∈II×tIICnJ
4 isphtpy2d.2 ⊢φ∧s∈01→sH0=F⁡s
5 isphtpy2d.3 ⊢φ∧s∈01→sH1=G⁡s
6 isphtpy2d.4 ⊢φ∧s∈01→0Hs=F⁡0
7 isphtpy2d.5 ⊢φ∧s∈01→1Hs=F⁡1
8 iitopon ⊢II∈TopOn⁡01
9 8 a1i ⊢φ→II∈TopOn⁡01
10 9 1 2 3 4 5 ishtpyd ⊢φ→H∈FIIHtpyJG
11 1 2 10 6 7 isphtpyd ⊢φ→H∈FPHtpy⁡JG