Theorem wlkcpr

Description: A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 2-Jan-2021)

	Ref	Expression
Assertion	wlkcpr	$$⊢W\in \mathrm{Walks}\left(G\right)\leftrightarrow 1^{st}\left(W\right)\mathrm{Walks}\left(G\right)2^{nd}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		wlkop	$$⊢W\in \mathrm{Walks}\left(G\right)\to W=⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩$$
2		wlkvv	$$⊢1^{st}\left(W\right)\mathrm{Walks}\left(G\right)2^{nd}\left(W\right)\to W\in \left(\mathrm{V}\times \mathrm{V}\right)$$
3		1st2ndb	$$⊢W\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow W=⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩$$
4	2 3	sylib	$$⊢1^{st}\left(W\right)\mathrm{Walks}\left(G\right)2^{nd}\left(W\right)\to W=⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩$$
5		eleq1	$$⊢W=⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩\to \left(W\in \mathrm{Walks}\left(G\right)\leftrightarrow ⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩\in \mathrm{Walks}\left(G\right)\right)$$
6		df-br	$$⊢1^{st}\left(W\right)\mathrm{Walks}\left(G\right)2^{nd}\left(W\right)\leftrightarrow ⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩\in \mathrm{Walks}\left(G\right)$$
7	5 6	bitr4di	$$⊢W=⟨1^{st}\left(W\right),2^{nd}\left(W\right)⟩\to \left(W\in \mathrm{Walks}\left(G\right)\leftrightarrow 1^{st}\left(W\right)\mathrm{Walks}\left(G\right)2^{nd}\left(W\right)\right)$$
8	1 4 7	pm5.21nii	$$⊢W\in \mathrm{Walks}\left(G\right)\leftrightarrow 1^{st}\left(W\right)\mathrm{Walks}\left(G\right)2^{nd}\left(W\right)$$