Metamath Proof Explorer

Theorem phtpyhtpy

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

Ref Expression
Hypotheses isphtpy.2 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
isphtpy.3 ${⊢}{\phi }\to {G}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
Assertion phtpyhtpy ${⊢}{\phi }\to {F}\mathrm{PHtpy}\left({J}\right){G}\subseteq {F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}$

Proof

Step Hyp Ref Expression
1 isphtpy.2 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
2 isphtpy.3 ${⊢}{\phi }\to {G}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
3 1 2 isphtpy ${⊢}{\phi }\to \left({h}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)↔\left({h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)\wedge \forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right)\right)$
4 simpl ${⊢}\left({h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)\wedge \forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right)\to {h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)$
5 3 4 syl6bi ${⊢}{\phi }\to \left({h}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)\to {h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)\right)$
6 5 ssrdv ${⊢}{\phi }\to {F}\mathrm{PHtpy}\left({J}\right){G}\subseteq {F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}$