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 e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) } )
2	1	relmptopab	|- Rel ( Paths ` G )