Theorem istrlson

Description: Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017) (Revised by AV, 7-Jan-2021) (Revised by AV, 21-Mar-2021)

	Ref	Expression
Hypothesis	trlsonfval.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	istrlson	$$⊢\left(\left(A\in V\wedge B\in V\right)\wedge \left(F\in U\wedge P\in Z\right)\right)\to \left(F\left(A\mathrm{TrailsOn}\left(G\right)B\right)P\leftrightarrow \left(F\left(A\mathrm{WalksOn}\left(G\right)B\right)P\wedge F\mathrm{Trails}\left(G\right)P\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		trlsonfval.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	trlsonfval	$$⊢\left(A\in V\wedge B\in V\right)\to A\mathrm{TrailsOn}\left(G\right)B=\left\{⟨f,p⟩|\left(f\left(A\mathrm{WalksOn}\left(G\right)B\right)p\wedge f\mathrm{Trails}\left(G\right)p\right)\right\}$$
3	2	breqd	$$⊢\left(A\in V\wedge B\in V\right)\to \left(F\left(A\mathrm{TrailsOn}\left(G\right)B\right)P\leftrightarrow F\left\{⟨f,p⟩|\left(f\left(A\mathrm{WalksOn}\left(G\right)B\right)p\wedge f\mathrm{Trails}\left(G\right)p\right)\right\}P\right)$$
4		breq12	$$⊢\left(f=F\wedge p=P\right)\to \left(f\left(A\mathrm{WalksOn}\left(G\right)B\right)p\leftrightarrow F\left(A\mathrm{WalksOn}\left(G\right)B\right)P\right)$$
5		breq12	$$⊢\left(f=F\wedge p=P\right)\to \left(f\mathrm{Trails}\left(G\right)p\leftrightarrow F\mathrm{Trails}\left(G\right)P\right)$$
6	4 5	anbi12d	$$⊢\left(f=F\wedge p=P\right)\to \left(\left(f\left(A\mathrm{WalksOn}\left(G\right)B\right)p\wedge f\mathrm{Trails}\left(G\right)p\right)\leftrightarrow \left(F\left(A\mathrm{WalksOn}\left(G\right)B\right)P\wedge F\mathrm{Trails}\left(G\right)P\right)\right)$$
7		eqid	$$⊢\left\{⟨f,p⟩|\left(f\left(A\mathrm{WalksOn}\left(G\right)B\right)p\wedge f\mathrm{Trails}\left(G\right)p\right)\right\}=\left\{⟨f,p⟩|\left(f\left(A\mathrm{WalksOn}\left(G\right)B\right)p\wedge f\mathrm{Trails}\left(G\right)p\right)\right\}$$
8	6 7	brabga	$$⊢\left(F\in U\wedge P\in Z\right)\to \left(F\left\{⟨f,p⟩|\left(f\left(A\mathrm{WalksOn}\left(G\right)B\right)p\wedge f\mathrm{Trails}\left(G\right)p\right)\right\}P\leftrightarrow \left(F\left(A\mathrm{WalksOn}\left(G\right)B\right)P\wedge F\mathrm{Trails}\left(G\right)P\right)\right)$$
9	3 8	sylan9bb	$$⊢\left(\left(A\in V\wedge B\in V\right)\wedge \left(F\in U\wedge P\in Z\right)\right)\to \left(F\left(A\mathrm{TrailsOn}\left(G\right)B\right)P\leftrightarrow \left(F\left(A\mathrm{WalksOn}\left(G\right)B\right)P\wedge F\mathrm{Trails}\left(G\right)P\right)\right)$$