Theorem isphtpy2d

Description: Deduction for membership in the class of path homotopies. (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 ) )
	isphtpy2d.1	|- ( ph -> H e. ( ( II tX II ) Cn J ) )
	isphtpy2d.2	|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 0 ) = ( F ` s ) )
	isphtpy2d.3	|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 1 ) = ( G ` s ) )
	isphtpy2d.4	|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` 0 ) )
	isphtpy2d.5	|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` 1 ) )
Assertion	isphtpy2d	|- ( ph -> H e. ( F ( PHtpy ` 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		isphtpy2d.1	|- ( ph -> H e. ( ( II tX II ) Cn J ) )
4		isphtpy2d.2	|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 0 ) = ( F ` s ) )
5		isphtpy2d.3	|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( s H 1 ) = ( G ` s ) )
6		isphtpy2d.4	|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 0 H s ) = ( F ` 0 ) )
7		isphtpy2d.5	|- ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 H s ) = ( F ` 1 ) )
8		iitopon	|- II e. ( TopOn ` ( 0 [,] 1 ) )
9	8	a1i	|- ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
10	9 1 2 3 4 5	ishtpyd	|- ( ph -> H e. ( F ( II Htpy J ) G ) )
11	1 2 10 6 7	isphtpyd	|- ( ph -> H e. ( F ( PHtpy ` J ) G ) )