Theorem ishtpyd

Description: Deduction for membership in the class of homotopies. (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 ) )
	ishtpyd.1	|- ( ph -> H e. ( ( J tX II ) Cn K ) )
	ishtpyd.2	|- ( ( ph /\ s e. X ) -> ( s H 0 ) = ( F ` s ) )
	ishtpyd.3	|- ( ( ph /\ s e. X ) -> ( s H 1 ) = ( G ` s ) )
Assertion	ishtpyd	|- ( ph -> H e. ( F ( J Htpy K ) G ) )

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		ishtpyd.1	|- ( ph -> H e. ( ( J tX II ) Cn K ) )
5		ishtpyd.2	|- ( ( ph /\ s e. X ) -> ( s H 0 ) = ( F ` s ) )
6		ishtpyd.3	|- ( ( ph /\ s e. X ) -> ( s H 1 ) = ( G ` s ) )
7	5 6	jca	|- ( ( ph /\ s e. X ) -> ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) )
8	7	ralrimiva	|- ( ph -> A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) )
9	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 ) ) ) ) )
10	4 8 9	mpbir2and	|- ( ph -> H e. ( F ( J Htpy K ) G ) )