Theorem isspth

Description: Conditions for a pair of classes/functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

	Ref	Expression
Assertion	isspth	|- ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )

Proof

Step	Hyp	Ref	Expression
1		spthsfval	|- ( SPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ Fun `' p ) }
2		cnveq	|- ( p = P -> `' p = `' P )
3	2	funeqd	|- ( p = P -> ( Fun `' p <-> Fun `' P ) )
4	3	adantl	|- ( ( f = F /\ p = P ) -> ( Fun `' p <-> Fun `' P ) )
5		reltrls	|- Rel ( Trails ` G )
6	1 4 5	brfvopabrbr	|- ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )