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

Definition df-pthon 26044
 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.)
Assertion
Ref Expression
df-pthon PathOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 Paths 𝑒)𝑝)}))
Distinct variable groups:   𝑣,𝑒,𝑓,𝑝   𝑎,𝑏,𝑒,𝑓,𝑝,𝑣

Detailed syntax breakdown of Definition df-pthon
StepHypRef Expression
1 cpthon 26032 . 2 class PathOn
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3173 . . 3 class V
5 va . . . 4 setvar 𝑎
6 vb . . . 4 setvar 𝑏
72cv 1474 . . . 4 class 𝑣
8 vf . . . . . . . 8 setvar 𝑓
98cv 1474 . . . . . . 7 class 𝑓
10 vp . . . . . . . 8 setvar 𝑝
1110cv 1474 . . . . . . 7 class 𝑝
125cv 1474 . . . . . . . 8 class 𝑎
136cv 1474 . . . . . . . 8 class 𝑏
143cv 1474 . . . . . . . . 9 class 𝑒
15 cwlkon 26030 . . . . . . . . 9 class WalkOn
167, 14, 15co 6549 . . . . . . . 8 class (𝑣 WalkOn 𝑒)
1712, 13, 16co 6549 . . . . . . 7 class (𝑎(𝑣 WalkOn 𝑒)𝑏)
189, 11, 17wbr 4583 . . . . . 6 wff 𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝
19 cpath 26028 . . . . . . . 8 class Paths
207, 14, 19co 6549 . . . . . . 7 class (𝑣 Paths 𝑒)
219, 11, 20wbr 4583 . . . . . 6 wff 𝑓(𝑣 Paths 𝑒)𝑝
2218, 21wa 383 . . . . 5 wff (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 Paths 𝑒)𝑝)
2322, 8, 10copab 4642 . . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 Paths 𝑒)𝑝)}
245, 6, 7, 7, 23cmpt2 6551 . . 3 class (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 Paths 𝑒)𝑝)})
252, 3, 4, 4, 24cmpt2 6551 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 Paths 𝑒)𝑝)}))
261, 25wceq 1475 1 wff PathOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝𝑓(𝑣 Paths 𝑒)𝑝)}))
 Colors of variables: wff setvar class This definition is referenced by:  pthon  26105  pthonprop  26107
 Copyright terms: Public domain W3C validator