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 ∈ II Cn J
isphtpy.3 ⊢ φ → G ∈ II Cn J
isphtpyd.1 ⊢ φ → H ∈ F II Htpy J G
isphtpyd.2 ⊢ φ ∧ s ∈ 0 1 → 0 H s = F ⁡ 0
isphtpyd.3 ⊢ φ ∧ s ∈ 0 1 → 1 H s = F ⁡ 1
Assertion isphtpyd ⊢ φ → H ∈ F PHtpy ⁡ J G

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢ φ → F ∈ II Cn J
2 isphtpy.3 ⊢ φ → G ∈ II Cn J
3 isphtpyd.1 ⊢ φ → H ∈ F II Htpy J G
4 isphtpyd.2 ⊢ φ ∧ s ∈ 0 1 → 0 H s = F ⁡ 0
5 isphtpyd.3 ⊢ φ ∧ s ∈ 0 1 → 1 H s = F ⁡ 1
6 4 5 jca ⊢ φ ∧ s ∈ 0 1 → 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
7 6 ralrimiva ⊢ φ → ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
8 1 2 isphtpy ⊢ φ → H ∈ F PHtpy ⁡ J G ↔ H ∈ F II Htpy J G ∧ ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
9 3 7 8 mpbir2and ⊢ φ → H ∈ F PHtpy ⁡ J G