Theorem htpycn

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

	Ref	Expression
Hypotheses	ishtpy.1	|- ( ph -> J e. ( TopOn ` X ) )
	ishtpy.3	|- ( ph -> F e. ( J Cn K ) )
	ishtpy.4	|- ( ph -> G e. ( J Cn K ) )
Assertion	htpycn	|- ( ph -> ( F ( J Htpy K ) G ) C_ ( ( J tX II ) Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		ishtpy.1	|- ( ph -> J e. ( TopOn ` X ) )
2		ishtpy.3	|- ( ph -> F e. ( J Cn K ) )
3		ishtpy.4	|- ( ph -> G e. ( J Cn K ) )
4	1 2 3	ishtpy	|- ( ph -> ( h e. ( F ( J Htpy K ) G ) <-> ( h e. ( ( J tX II ) Cn K ) /\ A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) ) ) )
5		simpl	|- ( ( h e. ( ( J tX II ) Cn K ) /\ A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) ) -> h e. ( ( J tX II ) Cn K ) )
6	4 5	syl6bi	|- ( ph -> ( h e. ( F ( J Htpy K ) G ) -> h e. ( ( J tX II ) Cn K ) ) )
7	6	ssrdv	|- ( ph -> ( F ( J Htpy K ) G ) C_ ( ( J tX II ) Cn K ) )