Metamath Proof Explorer

Theorem ishtpyd

Description: Deduction for membership in the class of homotopies. (Contributed by Mario Carneiro, 22-Feb-2015)

Ref Expression
Hypotheses ishtpy.1 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
ishtpy.3 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
ishtpy.4 ${⊢}{\phi }\to {G}\in \left({J}\mathrm{Cn}{K}\right)$
ishtpyd.1 ${⊢}{\phi }\to {H}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)$
ishtpyd.2 ${⊢}\left({\phi }\wedge {s}\in {X}\right)\to {s}{H}0={F}\left({s}\right)$
ishtpyd.3 ${⊢}\left({\phi }\wedge {s}\in {X}\right)\to {s}{H}1={G}\left({s}\right)$
Assertion ishtpyd ${⊢}{\phi }\to {H}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){G}\right)$

Proof

Step Hyp Ref Expression
1 ishtpy.1 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
2 ishtpy.3 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
3 ishtpy.4 ${⊢}{\phi }\to {G}\in \left({J}\mathrm{Cn}{K}\right)$
4 ishtpyd.1 ${⊢}{\phi }\to {H}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)$
5 ishtpyd.2 ${⊢}\left({\phi }\wedge {s}\in {X}\right)\to {s}{H}0={F}\left({s}\right)$
6 ishtpyd.3 ${⊢}\left({\phi }\wedge {s}\in {X}\right)\to {s}{H}1={G}\left({s}\right)$
7 5 6 jca ${⊢}\left({\phi }\wedge {s}\in {X}\right)\to \left({s}{H}0={F}\left({s}\right)\wedge {s}{H}1={G}\left({s}\right)\right)$
8 7 ralrimiva ${⊢}{\phi }\to \forall {s}\in {X}\phantom{\rule{.4em}{0ex}}\left({s}{H}0={F}\left({s}\right)\wedge {s}{H}1={G}\left({s}\right)\right)$
9 1 2 3 ishtpy ${⊢}{\phi }\to \left({H}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){G}\right)↔\left({H}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)\wedge \forall {s}\in {X}\phantom{\rule{.4em}{0ex}}\left({s}{H}0={F}\left({s}\right)\wedge {s}{H}1={G}\left({s}\right)\right)\right)\right)$
10 4 8 9 mpbir2and ${⊢}{\phi }\to {H}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){G}\right)$