MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wlkson Structured version   Visualization version   GIF version

Definition df-wlkson 28854
Description: Define the collection of walks with particular endpoints (in a hypergraph). The predicate 𝐹(𝐴(WalksOnβ€˜πΊ)𝐡)𝑃 can be read as "The pair ⟨𝐹, π‘ƒβŸ© represents a walk from vertex 𝐴 to vertex 𝐡 in a graph 𝐺", see also iswlkon 28911. This corresponds to the "x0-x(l)-walks", see Definition in [Bollobas] p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
Assertion
Ref Expression
df-wlkson WalksOn = (𝑔 ∈ V ↦ (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Walksβ€˜π‘”)𝑝 ∧ (π‘β€˜0) = π‘Ž ∧ (π‘β€˜(β™―β€˜π‘“)) = 𝑏)}))
Distinct variable groups:   𝑓,𝑔,𝑝   π‘Ž,𝑏,𝑓,𝑔,𝑝

Detailed syntax breakdown of Definition df-wlkson
StepHypRef Expression
1 cwlkson 28851 . 2 class WalksOn
2 vg . . 3 setvar 𝑔
3 cvv 3474 . . 3 class V
4 va . . . 4 setvar π‘Ž
5 vb . . . 4 setvar 𝑏
62cv 1540 . . . . 5 class 𝑔
7 cvtx 28253 . . . . 5 class Vtx
86, 7cfv 6543 . . . 4 class (Vtxβ€˜π‘”)
9 vf . . . . . . . 8 setvar 𝑓
109cv 1540 . . . . . . 7 class 𝑓
11 vp . . . . . . . 8 setvar 𝑝
1211cv 1540 . . . . . . 7 class 𝑝
13 cwlks 28850 . . . . . . . 8 class Walks
146, 13cfv 6543 . . . . . . 7 class (Walksβ€˜π‘”)
1510, 12, 14wbr 5148 . . . . . 6 wff 𝑓(Walksβ€˜π‘”)𝑝
16 cc0 11109 . . . . . . . 8 class 0
1716, 12cfv 6543 . . . . . . 7 class (π‘β€˜0)
184cv 1540 . . . . . . 7 class π‘Ž
1917, 18wceq 1541 . . . . . 6 wff (π‘β€˜0) = π‘Ž
20 chash 14289 . . . . . . . . 9 class β™―
2110, 20cfv 6543 . . . . . . . 8 class (β™―β€˜π‘“)
2221, 12cfv 6543 . . . . . . 7 class (π‘β€˜(β™―β€˜π‘“))
235cv 1540 . . . . . . 7 class 𝑏
2422, 23wceq 1541 . . . . . 6 wff (π‘β€˜(β™―β€˜π‘“)) = 𝑏
2515, 19, 24w3a 1087 . . . . 5 wff (𝑓(Walksβ€˜π‘”)𝑝 ∧ (π‘β€˜0) = π‘Ž ∧ (π‘β€˜(β™―β€˜π‘“)) = 𝑏)
2625, 9, 11copab 5210 . . . 4 class {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Walksβ€˜π‘”)𝑝 ∧ (π‘β€˜0) = π‘Ž ∧ (π‘β€˜(β™―β€˜π‘“)) = 𝑏)}
274, 5, 8, 8, 26cmpo 7410 . . 3 class (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Walksβ€˜π‘”)𝑝 ∧ (π‘β€˜0) = π‘Ž ∧ (π‘β€˜(β™―β€˜π‘“)) = 𝑏)})
282, 3, 27cmpt 5231 . 2 class (𝑔 ∈ V ↦ (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Walksβ€˜π‘”)𝑝 ∧ (π‘β€˜0) = π‘Ž ∧ (π‘β€˜(β™―β€˜π‘“)) = 𝑏)}))
291, 28wceq 1541 1 wff WalksOn = (𝑔 ∈ V ↦ (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(Walksβ€˜π‘”)𝑝 ∧ (π‘β€˜0) = π‘Ž ∧ (π‘β€˜(β™―β€˜π‘“)) = 𝑏)}))
Colors of variables: wff setvar class
This definition is referenced by:  wlkson  28910  wlkonprop  28912
  Copyright terms: Public domain W3C validator