Metamath Proof Explorer


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

Proof

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