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

Metamath Proof Explorer

Theorem relpths

Description: The set ( PathsG ) of all paths on G is a set of pairs by our definition of a path, and so is a relation. (Contributed by AV, 30-Oct-2021)

		Ref	Expression
	Assertion	relpths	$⊢ Rel Paths (G)$

Proof

Step	Hyp	Ref	Expression
1		df-pths	$⊢ Paths = (g \in V ⟼ \{⟨f, p⟩ \| (f Trails (g) p \land Fun {({p ↾}_{(1 ..^\|f\|)})}^{-1} \land p [\{0, \|f\|\}] \cap p [(1 ..^\|f\|)] = \emptyset)\})$
2	1	relmptopab	$⊢ Rel Paths (G)$