Metamath Proof Explorer

Theorem phtpyhtpy

Description: A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses isphtpy.2 ⊢ φ → F ∈ II Cn J
isphtpy.3 ⊢ φ → G ∈ II Cn J
Assertion phtpyhtpy ⊢ φ → F PHtpy ⁡ J G ⊆ F II Htpy J G

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢ φ → F ∈ II Cn J
2 isphtpy.3 ⊢ φ → G ∈ II Cn J
3 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
4 simpl ⊢ h ∈ F II Htpy J G ∧ ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1 → h ∈ F II Htpy J G
5 3 4 biimtrdi ⊢ φ → h ∈ F PHtpy ⁡ J G → h ∈ F II Htpy J G
6 5 ssrdv ⊢ φ → F PHtpy ⁡ J G ⊆ F II Htpy J G