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

Definition df-wlkon 25808
Description: Define the collection of walks with particular endpoints (in an un- directed graph). 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.)
Assertion
Ref Expression
df-wlkon WalkOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))
Distinct variable groups:   𝑣,𝑒,𝑓,𝑝   𝑎,𝑏,𝑒,𝑓,𝑝,𝑣

Detailed syntax breakdown of Definition df-wlkon
StepHypRef Expression
1 cwlkon 25796 . 2 class WalkOn
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3172 . . 3 class V
5 va . . . 4 setvar 𝑎
6 vb . . . 4 setvar 𝑏
72cv 1473 . . . 4 class 𝑣
8 vf . . . . . . . 8 setvar 𝑓
98cv 1473 . . . . . . 7 class 𝑓
10 vp . . . . . . . 8 setvar 𝑝
1110cv 1473 . . . . . . 7 class 𝑝
123cv 1473 . . . . . . . 8 class 𝑒
13 cwalk 25792 . . . . . . . 8 class Walks
147, 12, 13co 6527 . . . . . . 7 class (𝑣 Walks 𝑒)
159, 11, 14wbr 4577 . . . . . 6 wff 𝑓(𝑣 Walks 𝑒)𝑝
16 cc0 9792 . . . . . . . 8 class 0
1716, 11cfv 5790 . . . . . . 7 class (𝑝‘0)
185cv 1473 . . . . . . 7 class 𝑎
1917, 18wceq 1474 . . . . . 6 wff (𝑝‘0) = 𝑎
20 chash 12934 . . . . . . . . 9 class #
219, 20cfv 5790 . . . . . . . 8 class (#‘𝑓)
2221, 11cfv 5790 . . . . . . 7 class (𝑝‘(#‘𝑓))
236cv 1473 . . . . . . 7 class 𝑏
2422, 23wceq 1474 . . . . . 6 wff (𝑝‘(#‘𝑓)) = 𝑏
2515, 19, 24w3a 1030 . . . . 5 wff (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)
2625, 8, 10copab 4636 . . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}
275, 6, 7, 7, 26cmpt2 6529 . . 3 class (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})
282, 3, 4, 4, 27cmpt2 6529 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))
291, 28wceq 1474 1 wff WalkOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))
Colors of variables: wff setvar class
This definition is referenced by:  wlkon  25827  wlkonprop  25829
  Copyright terms: Public domain W3C validator