Theorem wlkop

Description: A walk is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018) (Revised by AV, 1-Jan-2021)

	Ref	Expression
Assertion	wlkop	$$⊢W\in \mathrm{Walks}\left(G\right)\to W=⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		relwlk	$$⊢\mathrm{Rel}\mathrm{Walks}\left(G\right)$$
2		1st2nd	$$⊢\left(\mathrm{Rel}\mathrm{Walks}\left(G\right)\wedge W\in \mathrm{Walks}\left(G\right)\right)\to W=⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩$$
3	1 2	mpan	$$⊢W\in \mathrm{Walks}\left(G\right)\to W=⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩$$