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	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) )

Step	Hyp	Ref	Expression
1		wlkop	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
2		wlkvv	⊢ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) → 𝑊 ∈ ( V × V ) )
3		1st2ndb	⊢ ( 𝑊 ∈ ( V × V ) ↔ 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
4	2 3	sylib	⊢ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
5		eleq1	⊢ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ → ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∈ ( Walks ‘ 𝐺 ) ) )
6		df-br	⊢ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ↔ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∈ ( Walks ‘ 𝐺 ) )
7	5 6	bitr4di	⊢ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ → ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ) )
8	1 4 7	pm5.21nii	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) )

Metamath Proof Explorer