Theorem phtpycn

Description: A path homotopy is a continuous function. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	isphtpy.2	|- ( ph -> F e. ( II Cn J ) )
	isphtpy.3	|- ( ph -> G e. ( II Cn J ) )
Assertion	phtpycn	|- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( ( II tX II ) Cn J ) )

Proof

Step	Hyp	Ref	Expression
1		isphtpy.2	|- ( ph -> F e. ( II Cn J ) )
2		isphtpy.3	|- ( ph -> G e. ( II Cn J ) )
3	1 2	phtpyhtpy	|- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( F ( II Htpy J ) G ) )
4		iitopon	|- II e. ( TopOn ` ( 0 [,] 1 ) )
5	4	a1i	|- ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
6	5 1 2	htpycn	|- ( ph -> ( F ( II Htpy J ) G ) C_ ( ( II tX II ) Cn J ) )
7	3 6	sstrd	|- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( ( II tX II ) Cn J ) )