Metamath Proof Explorer


Theorem ishtpyd

Description: Deduction for membership in the class of homotopies. (Contributed by Mario Carneiro, 22-Feb-2015)

Ref Expression
Hypotheses ishtpy.1 φJTopOnX
ishtpy.3 φFJCnK
ishtpy.4 φGJCnK
ishtpyd.1 φHJ×tIICnK
ishtpyd.2 φsXsH0=Fs
ishtpyd.3 φsXsH1=Gs
Assertion ishtpyd φHFJHtpyKG

Proof

Step Hyp Ref Expression
1 ishtpy.1 φJTopOnX
2 ishtpy.3 φFJCnK
3 ishtpy.4 φGJCnK
4 ishtpyd.1 φHJ×tIICnK
5 ishtpyd.2 φsXsH0=Fs
6 ishtpyd.3 φsXsH1=Gs
7 5 6 jca φsXsH0=FssH1=Gs
8 7 ralrimiva φsXsH0=FssH1=Gs
9 1 2 3 ishtpy φHFJHtpyKGHJ×tIICnKsXsH0=FssH1=Gs
10 4 8 9 mpbir2and φHFJHtpyKG