Description: The set ( WalksG ) of all walks on G is a set of pairs by our definition of a walk, and so is a relation. (Contributed by Alexander van der Vekens, 30-Jun-2018) (Revised by AV, 19-Feb-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | relwlk | ⊢ Rel ( Walks ‘ 𝐺 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-wlks | ⊢ Walks = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ) | |
| 2 | 1 | relmptopab | ⊢ Rel ( Walks ‘ 𝐺 ) |