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

Definition df-trlson 40901
Description: Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
Assertion
Ref Expression
df-trlson TrailsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝𝑓(TrailS‘𝑔)𝑝)}))
Distinct variable groups:   𝑓,𝑔,𝑝   𝑎,𝑏,𝑓,𝑔,𝑝

Detailed syntax breakdown of Definition df-trlson
StepHypRef Expression
1 ctrlson 40899 . 2 class TrailsOn
2 vg . . 3 setvar 𝑔
3 cvv 3169 . . 3 class V
4 va . . . 4 setvar 𝑎
5 vb . . . 4 setvar 𝑏
62cv 1473 . . . . 5 class 𝑔
7 cvtx 40228 . . . . 5 class Vtx
86, 7cfv 5787 . . . 4 class (Vtx‘𝑔)
9 vf . . . . . . . 8 setvar 𝑓
109cv 1473 . . . . . . 7 class 𝑓
11 vp . . . . . . . 8 setvar 𝑝
1211cv 1473 . . . . . . 7 class 𝑝
134cv 1473 . . . . . . . 8 class 𝑎
145cv 1473 . . . . . . . 8 class 𝑏
15 cwlkson 40797 . . . . . . . . 9 class WalksOn
166, 15cfv 5787 . . . . . . . 8 class (WalksOn‘𝑔)
1713, 14, 16co 6524 . . . . . . 7 class (𝑎(WalksOn‘𝑔)𝑏)
1810, 12, 17wbr 4574 . . . . . 6 wff 𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝
19 ctrls 40898 . . . . . . . 8 class TrailS
206, 19cfv 5787 . . . . . . 7 class (TrailS‘𝑔)
2110, 12, 20wbr 4574 . . . . . 6 wff 𝑓(TrailS‘𝑔)𝑝
2218, 21wa 382 . . . . 5 wff (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝𝑓(TrailS‘𝑔)𝑝)
2322, 9, 11copab 4633 . . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝𝑓(TrailS‘𝑔)𝑝)}
244, 5, 8, 8, 23cmpt2 6526 . . 3 class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝𝑓(TrailS‘𝑔)𝑝)})
252, 3, 24cmpt 4634 . 2 class (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝𝑓(TrailS‘𝑔)𝑝)}))
261, 25wceq 1474 1 wff TrailsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝𝑓(TrailS‘𝑔)𝑝)}))
Colors of variables: wff setvar class
This definition is referenced by:  trlsonfval  40912  trlsonprop  40914
  Copyright terms: Public domain W3C validator