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

Definition df-spthson 29485
Description: Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 9-Jan-2021.)
Assertion
Ref Expression
df-spthson SPathsOn = (𝑔 ∈ V ↦ (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(SPathsβ€˜π‘”)𝑝)}))
Distinct variable groups:   𝑓,𝑔,𝑝   π‘Ž,𝑏,𝑔,𝑓,𝑝

Detailed syntax breakdown of Definition df-spthson
StepHypRef Expression
1 cspthson 29481 . 2 class SPathsOn
2 vg . . 3 setvar 𝑔
3 cvv 3468 . . 3 class V
4 va . . . 4 setvar π‘Ž
5 vb . . . 4 setvar 𝑏
62cv 1532 . . . . 5 class 𝑔
7 cvtx 28764 . . . . 5 class Vtx
86, 7cfv 6537 . . . 4 class (Vtxβ€˜π‘”)
9 vf . . . . . . . 8 setvar 𝑓
109cv 1532 . . . . . . 7 class 𝑓
11 vp . . . . . . . 8 setvar 𝑝
1211cv 1532 . . . . . . 7 class 𝑝
134cv 1532 . . . . . . . 8 class π‘Ž
145cv 1532 . . . . . . . 8 class 𝑏
15 ctrlson 29457 . . . . . . . . 9 class TrailsOn
166, 15cfv 6537 . . . . . . . 8 class (TrailsOnβ€˜π‘”)
1713, 14, 16co 7405 . . . . . . 7 class (π‘Ž(TrailsOnβ€˜π‘”)𝑏)
1810, 12, 17wbr 5141 . . . . . 6 wff 𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝
19 cspths 29479 . . . . . . . 8 class SPaths
206, 19cfv 6537 . . . . . . 7 class (SPathsβ€˜π‘”)
2110, 12, 20wbr 5141 . . . . . 6 wff 𝑓(SPathsβ€˜π‘”)𝑝
2218, 21wa 395 . . . . 5 wff (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(SPathsβ€˜π‘”)𝑝)
2322, 9, 11copab 5203 . . . 4 class {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(SPathsβ€˜π‘”)𝑝)}
244, 5, 8, 8, 23cmpo 7407 . . 3 class (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(SPathsβ€˜π‘”)𝑝)})
252, 3, 24cmpt 5224 . 2 class (𝑔 ∈ V ↦ (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(SPathsβ€˜π‘”)𝑝)}))
261, 25wceq 1533 1 wff SPathsOn = (𝑔 ∈ V ↦ (π‘Ž ∈ (Vtxβ€˜π‘”), 𝑏 ∈ (Vtxβ€˜π‘”) ↦ {βŸ¨π‘“, π‘βŸ© ∣ (𝑓(π‘Ž(TrailsOnβ€˜π‘”)𝑏)𝑝 ∧ 𝑓(SPathsβ€˜π‘”)𝑝)}))
Colors of variables: wff setvar class
This definition is referenced by:  spthson  29507  spthonprop  29511
  Copyright terms: Public domain W3C validator