Theorem phtpyhtpy

Description: A path homotopy is a homotopy. (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	phtpyhtpy	|- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( F ( II Htpy J ) G ) )

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	isphtpy	|- ( ph -> ( h e. ( F ( PHtpy ` J ) G ) <-> ( h e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) ) ) )
4		simpl	|- ( ( h e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( F ` 0 ) /\ ( 1 h s ) = ( F ` 1 ) ) ) -> h e. ( F ( II Htpy J ) G ) )
5	3 4	syl6bi	|- ( ph -> ( h e. ( F ( PHtpy ` J ) G ) -> h e. ( F ( II Htpy J ) G ) ) )
6	5	ssrdv	|- ( ph -> ( F ( PHtpy ` J ) G ) C_ ( F ( II Htpy J ) G ) )