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 ‘ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		df-phtpc	⊢ ≃ph = ( 𝑥 ∈ Top ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( II Cn 𝑥 ) ∧ ( 𝑓 ( PHtpy ‘ 𝑥 ) 𝑔 ) ≠ ∅ ) } )
2	1	relmptopab	⊢ Rel ( ≃ph ‘ 𝐽 )