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

Definition df-spthon 25838
Description: Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
Assertion
Ref Expression
df-spthon SPathOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 SPaths 𝑒)𝑝)}))
Distinct variable groups:   𝑣,𝑒,𝑓,𝑝   𝑎,𝑏,𝑒,𝑓,𝑝,𝑣

Detailed syntax breakdown of Definition df-spthon
StepHypRef Expression
1 cspthon 25826 . 2 class SPathOn
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 𝑝
125cv 1473 . . . . . . . 8 class 𝑎
136cv 1473 . . . . . . . 8 class 𝑏
143cv 1473 . . . . . . . . 9 class 𝑒
15 cwlkon 25823 . . . . . . . . 9 class WalkOn
167, 14, 15co 6526 . . . . . . . 8 class (𝑣 WalkOn 𝑒)
1712, 13, 16co 6526 . . . . . . 7 class (𝑎(𝑣 WalkOn 𝑒)𝑏)
189, 11, 17wbr 4577 . . . . . 6 wff 𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝
19 cspath 25822 . . . . . . . 8 class SPaths
207, 14, 19co 6526 . . . . . . 7 class (𝑣 SPaths 𝑒)
219, 11, 20wbr 4577 . . . . . 6 wff 𝑓(𝑣 SPaths 𝑒)𝑝
2218, 21wa 382 . . . . 5 wff (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 SPaths 𝑒)𝑝)
2322, 8, 10copab 4636 . . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 SPaths 𝑒)𝑝)}
245, 6, 7, 7, 23cmpt2 6528 . . 3 class (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 SPaths 𝑒)𝑝)})
252, 3, 4, 4, 24cmpt2 6528 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 SPaths 𝑒)𝑝)}))
261, 25wceq 1474 1 wff SPathOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 SPaths 𝑒)𝑝)}))
Colors of variables: wff setvar class
This definition is referenced by:  spthon  25905  spthonprp  25908
  Copyright terms: Public domain W3C validator