# 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 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
isphtpy.3 ${⊢}{\phi }\to {G}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
isphtpyd.1 ${⊢}{\phi }\to {H}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)$
isphtpyd.2 ${⊢}\left({\phi }\wedge {s}\in \left[0,1\right]\right)\to 0{H}{s}={F}\left(0\right)$
isphtpyd.3 ${⊢}\left({\phi }\wedge {s}\in \left[0,1\right]\right)\to 1{H}{s}={F}\left(1\right)$
Assertion isphtpyd ${⊢}{\phi }\to {H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)$

### 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 isphtpyd.1 ${⊢}{\phi }\to {H}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)$
4 isphtpyd.2 ${⊢}\left({\phi }\wedge {s}\in \left[0,1\right]\right)\to 0{H}{s}={F}\left(0\right)$
5 isphtpyd.3 ${⊢}\left({\phi }\wedge {s}\in \left[0,1\right]\right)\to 1{H}{s}={F}\left(1\right)$
6 4 5 jca ${⊢}\left({\phi }\wedge {s}\in \left[0,1\right]\right)\to \left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)$
7 6 ralrimiva ${⊢}{\phi }\to \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)$
8 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)$
9 3 7 8 mpbir2and ${⊢}{\phi }\to {H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)$