This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reltrls

Description: The set ( TrailsG ) of all trails on G is a set of pairs by our definition of a trail, and so is a relation. (Contributed by AV, 29-Oct-2021)

		Ref	Expression
	Assertion	reltrls	$⊢ Rel Trails (G)$

Proof

Step	Hyp	Ref	Expression
1		df-trls	$⊢ Trails = (g \in V ⟼ \{⟨f, p⟩ \| (f Walks (g) p \land Fun f^{-1})\})$
2	1	relmptopab	$⊢ Rel Trails (G)$