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\mathrm{SPaths}\left(G\right)P\leftrightarrow \left(F\mathrm{Trails}\left(G\right)P\wedge \mathrm{Fun}{P}^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		spthsfval	$$⊢\mathrm{SPaths}\left(G\right)=\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(G\right)p\wedge \mathrm{Fun}{p}^{-1}\right)\right\}$$
2		cnveq	$$⊢p=P\to p^{-1}=P^{-1}$$
3	2	funeqd	$$⊢p=P\to \left(\mathrm{Fun}{p}^{-1}\leftrightarrow \mathrm{Fun}{P}^{-1}\right)$$
4	3	adantl	$$⊢\left(f=F\wedge p=P\right)\to \left(\mathrm{Fun}{p}^{-1}\leftrightarrow \mathrm{Fun}{P}^{-1}\right)$$
5		reltrls	$$⊢\mathrm{Rel}\mathrm{Trails}\left(G\right)$$
6	1 4 5	brfvopabrbr	$$⊢F\mathrm{SPaths}\left(G\right)P\leftrightarrow \left(F\mathrm{Trails}\left(G\right)P\wedge \mathrm{Fun}{P}^{-1}\right)$$