Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wlkson Structured version   Visualization version   GIF version

Definition df-wlkson 40802
 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 40865. 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‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(1Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))
Distinct variable groups:   𝑓,𝑔,𝑝   𝑎,𝑏,𝑓,𝑔,𝑝

Detailed syntax breakdown of Definition df-wlkson
StepHypRef Expression
1 cwlkson 40798 . 2 class WalksOn
2 vg . . 3 setvar 𝑔
3 cvv 3173 . . 3 class V
4 va . . . 4 setvar 𝑎
5 vb . . . 4 setvar 𝑏
62cv 1474 . . . . 5 class 𝑔
7 cvtx 25673 . . . . 5 class Vtx
86, 7cfv 5804 . . . 4 class (Vtx‘𝑔)
9 vf . . . . . . . 8 setvar 𝑓
109cv 1474 . . . . . . 7 class 𝑓
11 vp . . . . . . . 8 setvar 𝑝
1211cv 1474 . . . . . . 7 class 𝑝
13 c1wlks 40796 . . . . . . . 8 class 1Walks
146, 13cfv 5804 . . . . . . 7 class (1Walks‘𝑔)
1510, 12, 14wbr 4583 . . . . . 6 wff 𝑓(1Walks‘𝑔)𝑝
16 cc0 9815 . . . . . . . 8 class 0
1716, 12cfv 5804 . . . . . . 7 class (𝑝‘0)
184cv 1474 . . . . . . 7 class 𝑎
1917, 18wceq 1475 . . . . . 6 wff (𝑝‘0) = 𝑎
20 chash 12979 . . . . . . . . 9 class #
2110, 20cfv 5804 . . . . . . . 8 class (#‘𝑓)
2221, 12cfv 5804 . . . . . . 7 class (𝑝‘(#‘𝑓))
235cv 1474 . . . . . . 7 class 𝑏
2422, 23wceq 1475 . . . . . 6 wff (𝑝‘(#‘𝑓)) = 𝑏
2515, 19, 24w3a 1031 . . . . 5 wff (𝑓(1Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)
2625, 9, 11copab 4642 . . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(1Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}
274, 5, 8, 8, 26cmpt2 6551 . . 3 class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(1Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})
282, 3, 27cmpt 4643 . 2 class (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(1Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))
291, 28wceq 1475 1 wff WalksOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(1Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))
 Colors of variables: wff setvar class This definition is referenced by:  wlkson  40864  wlkOnprop  40866
 Copyright terms: Public domain W3C validator