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	$$⊢\mathrm{Rel}{\simeq }_{\mathrm{ph}}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-phtpc	$$⊢{\simeq }_{\mathrm{ph}}=\left(x\in \mathrm{Top}⟼\left\{⟨f,g⟩|\left(\left\{f,g\right\}\subseteq \mathrm{II}\mathrm{Cn}x\wedge f\mathrm{PHtpy}\left(x\right)g\ne \varnothing \right)\right\}\right)$$
2	1	relmptopab	$$⊢\mathrm{Rel}{\simeq }_{\mathrm{ph}}\left(J\right)$$