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 Walks (G) \leftrightarrow 1^{st} (W) Walks (G) 2^{nd} (W)$

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

Metamath Proof Explorer