Definition df-spthon 26045

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

Step	Hyp	Ref	Expression
1		cspthon 26033	. 2 class SPathOn
2		vv	. . 3 setvar 𝑣
3		ve	. . 3 setvar 𝑒
4		cvv 3173	. . 3 class V
5		va	. . . 4 setvar 𝑎
6		vb	. . . 4 setvar 𝑏
7	2	cv 1474	. . . 4 class 𝑣
8		vf	. . . . . . . 8 setvar 𝑓
9	8	cv 1474	. . . . . . 7 class 𝑓
10		vp	. . . . . . . 8 setvar 𝑝
11	10	cv 1474	. . . . . . 7 class 𝑝
12	5	cv 1474	. . . . . . . 8 class 𝑎
13	6	cv 1474	. . . . . . . 8 class 𝑏
14	3	cv 1474	. . . . . . . . 9 class 𝑒
15		cwlkon 26030	. . . . . . . . 9 class WalkOn
16	7, 14, 15	co 6549	. . . . . . . 8 class (𝑣 WalkOn 𝑒)
17	12, 13, 16	co 6549	. . . . . . 7 class (𝑎(𝑣 WalkOn 𝑒)𝑏)
18	9, 11, 17	wbr 4583	. . . . . 6 wff 𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝
19		cspath 26029	. . . . . . . 8 class SPaths
20	7, 14, 19	co 6549	. . . . . . 7 class (𝑣 SPaths 𝑒)
21	9, 11, 20	wbr 4583	. . . . . 6 wff 𝑓(𝑣 SPaths 𝑒)𝑝
22	18, 21	wa 383	. . . . 5 wff (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 SPaths 𝑒)𝑝)
23	22, 8, 10	copab 4642	. . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 SPaths 𝑒)𝑝)}
24	5, 6, 7, 7, 23	cmpt2 6551	. . 3 class (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 SPaths 𝑒)𝑝)})
25	2, 3, 4, 4, 24	cmpt2 6551	. 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 SPaths 𝑒)𝑝)}))
26	1, 25	wceq 1475	1 wff SPathOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 SPaths 𝑒)𝑝)}))

This definition is referenced by:  spthon  26112  spthonprp  26115