Theorem istrl

Description: Conditions for a pair of classes/functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 28-Dec-2020) (Revised by AV, 29-Oct-2021)

	Ref	Expression
Assertion	istrl	$$⊢F\mathrm{Trails}\left(G\right)P\leftrightarrow \left(F\mathrm{Walks}\left(G\right)P\wedge \mathrm{Fun}{F}^{-1}\right)$$

Proof

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