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{\times }_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)\leftrightarrow \left(h\in \left(\left(J{\times }_t\mathrm{II}\right)\mathrm{Cn}K\right)\wedge \forall s\in X\left(sh0=F\left(s\right)\wedge sh1=G\left(s\right)\right)\right)\right)$$
5		simpl	$$⊢\left(h\in \left(\left(J{\times }_t\mathrm{II}\right)\mathrm{Cn}K\right)\wedge \forall s\in X\left(sh0=F\left(s\right)\wedge sh1=G\left(s\right)\right)\right)\to h\in \left(\left(J{\times }_t\mathrm{II}\right)\mathrm{Cn}K\right)$$
6	4 5	biimtrdi	$$⊢\phi \to \left(h\in \left(F\left(J\mathrm{Htpy}K\right)G\right)\to h\in \left(\left(J{\times }_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{\times }_t\mathrm{II}\right)\mathrm{Cn}K$$