Theorem phtpycn

Description: A path homotopy is a continuous function. (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	phtpycn	$$⊢\phi \to F\mathrm{PHtpy}\left(J\right)G\subseteq \left(\mathrm{II}{\times }_t\mathrm{II}\right)\mathrm{Cn}J$$

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	phtpyhtpy	$$⊢\phi \to F\mathrm{PHtpy}\left(J\right)G\subseteq F\left(\mathrm{II}\mathrm{Htpy}J\right)G$$
4		iitopon	$$⊢\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$$
5	4	a1i	$$⊢\phi \to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$$
6	5 1 2	htpycn	$$⊢\phi \to F\left(\mathrm{II}\mathrm{Htpy}J\right)G\subseteq \left(\mathrm{II}{\times }_t\mathrm{II}\right)\mathrm{Cn}J$$
7	3 6	sstrd	$$⊢\phi \to F\mathrm{PHtpy}\left(J\right)G\subseteq \left(\mathrm{II}{\times }_t\mathrm{II}\right)\mathrm{Cn}J$$