# Metamath Proof Explorer

## Theorem htpycn

Description: A homotopy is a continuous function. (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)$
Assertion htpycn ${⊢}{\phi }\to {F}\left({J}\mathrm{Htpy}{K}\right){G}\subseteq \left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}$

### 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 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)$
5 simpl ${⊢}\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)\to {h}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)$
6 4 5 syl6bi ${⊢}{\phi }\to \left({h}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){G}\right)\to {h}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)\right)$
7 6 ssrdv ${⊢}{\phi }\to {F}\left({J}\mathrm{Htpy}{K}\right){G}\subseteq \left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}$