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 ∈ II Cn J
isphtpy.3 ⊢ φ → G ∈ II Cn J
isphtpy2d.1 ⊢ φ → H ∈ II × t II Cn J
isphtpy2d.2 ⊢ φ ∧ s ∈ 0 1 → s H 0 = F ⁡ s
isphtpy2d.3 ⊢ φ ∧ s ∈ 0 1 → s H 1 = G ⁡ s
isphtpy2d.4 ⊢ φ ∧ s ∈ 0 1 → 0 H s = F ⁡ 0
isphtpy2d.5 ⊢ φ ∧ s ∈ 0 1 → 1 H s = F ⁡ 1
Assertion isphtpy2d ⊢ φ → 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 isphtpy2d.1 ⊢ φ → H ∈ II × t II Cn J
4 isphtpy2d.2 ⊢ φ ∧ s ∈ 0 1 → s H 0 = F ⁡ s
5 isphtpy2d.3 ⊢ φ ∧ s ∈ 0 1 → s H 1 = G ⁡ s
6 isphtpy2d.4 ⊢ φ ∧ s ∈ 0 1 → 0 H s = F ⁡ 0
7 isphtpy2d.5 ⊢ φ ∧ s ∈ 0 1 → 1 H s = F ⁡ 1
8 iitopon ⊢ II ∈ TopOn ⁡ 0 1
9 8 a1i ⊢ φ → II ∈ TopOn ⁡ 0 1
10 9 1 2 3 4 5 ishtpyd ⊢ φ → H ∈ F II Htpy J G
11 1 2 10 6 7 isphtpyd ⊢ φ → H ∈ F PHtpy ⁡ J G