This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )

Step	Hyp	Ref	Expression
1		relwlk	⊢ Rel ( Walks ‘ 𝐺 )
2		1st2nd	⊢ ( ( Rel ( Walks ‘ 𝐺 ) ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
3	1 2	mpan	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )