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

Definition df-pthson 28972
Description: Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.)
Assertion
Ref Expression
df-pthson PathsOn = (𝑔 ∈ V ↦ (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(Pathsβ€˜π‘”)𝑝)}))
Distinct variable groups:   𝑓,𝑔,𝑝   π‘Ž,𝑏,𝑔,𝑓,𝑝

Detailed syntax breakdown of Definition df-pthson
StepHypRef Expression
1 cpthson 28968 . 2 class PathsOn
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 𝑝
134cv 1540 . . . . . . . 8 class π‘Ž
145cv 1540 . . . . . . . 8 class 𝑏
15 ctrlson 28945 . . . . . . . . 9 class TrailsOn
166, 15cfv 6543 . . . . . . . 8 class (TrailsOnβ€˜π‘”)
1713, 14, 16co 7408 . . . . . . 7 class (π‘Ž(TrailsOnβ€˜π‘”)𝑏)
1810, 12, 17wbr 5148 . . . . . 6 wff 𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝
19 cpths 28966 . . . . . . . 8 class Paths
206, 19cfv 6543 . . . . . . 7 class (Pathsβ€˜π‘”)
2110, 12, 20wbr 5148 . . . . . 6 wff 𝑓(Pathsβ€˜π‘”)𝑝
2218, 21wa 396 . . . . 5 wff (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(Pathsβ€˜π‘”)𝑝)
2322, 9, 11copab 5210 . . . 4 class {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(Pathsβ€˜π‘”)𝑝)}
244, 5, 8, 8, 23cmpo 7410 . . 3 class (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(Pathsβ€˜π‘”)𝑝)})
252, 3, 24cmpt 5231 . 2 class (𝑔 ∈ V ↦ (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(Pathsβ€˜π‘”)𝑝)}))
261, 25wceq 1541 1 wff PathsOn = (𝑔 ∈ V ↦ (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(Pathsβ€˜π‘”)𝑝)}))
Colors of variables: wff setvar class
This definition is referenced by:  pthsonfval  28994  pthsonprop  28998
  Copyright terms: Public domain W3C validator