Metamath Proof Explorer

Theorem phtpcrel

Description: The path homotopy relation is a relation. (Contributed by Mario Carneiro, 7-Jun-2014) (Revised by Mario Carneiro, 7-Aug-2014)

Ref Expression
Assertion phtpcrel 
|- Rel ( ~=ph ` J )

Proof

Step Hyp Ref Expression
1 df-phtpc 
 |-  ~=ph = ( x e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn x ) /\ ( f ( PHtpy ` x ) g ) =/= (/) ) } )
2 1 relmptopab 
 |-  Rel ( ~=ph ` J )