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 ⊢φ→F∈IICnJ
isphtpy.3 ⊢φ→G∈IICnJ
isphtpyd.1 ⊢φ→H∈FIIHtpyJG
isphtpyd.2 ⊢φ∧s∈01→0Hs=F⁡0
isphtpyd.3 ⊢φ∧s∈01→1Hs=F⁡1
Assertion isphtpyd ⊢φ→H∈FPHtpy⁡JG

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢φ→F∈IICnJ
2 isphtpy.3 ⊢φ→G∈IICnJ
3 isphtpyd.1 ⊢φ→H∈FIIHtpyJG
4 isphtpyd.2 ⊢φ∧s∈01→0Hs=F⁡0
5 isphtpyd.3 ⊢φ∧s∈01→1Hs=F⁡1
6 4 5 jca ⊢φ∧s∈01→0Hs=F⁡0∧1Hs=F⁡1
7 6 ralrimiva ⊢φ→∀s∈010Hs=F⁡0∧1Hs=F⁡1
8 1 2 isphtpy ⊢φ→H∈FPHtpy⁡JG↔H∈FIIHtpyJG∧∀s∈010Hs=F⁡0∧1Hs=F⁡1
9 3 7 8 mpbir2and ⊢φ→H∈FPHtpy⁡JG