Definition df-trlson 40902

Description: Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)

Assertion

Ref	Expression
df-trlson	⊢ TrailsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(TrailS‘𝑔)𝑝)}))

Distinct variable groups:   𝑓,𝑔,𝑝   𝑎,𝑏,𝑓,𝑔,𝑝

Detailed syntax breakdown of Definition df-trlson

Step	Hyp	Ref	Expression
1		ctrlson 40900	. 2 class TrailsOn
2		vg	. . 3 setvar 𝑔
3		cvv 3173	. . 3 class V
4		va	. . . 4 setvar 𝑎
5		vb	. . . 4 setvar 𝑏
6	2	cv 1474	. . . . 5 class 𝑔
7		cvtx 25673	. . . . 5 class Vtx
8	6, 7	cfv 5804	. . . 4 class (Vtx‘𝑔)
9		vf	. . . . . . . 8 setvar 𝑓
10	9	cv 1474	. . . . . . 7 class 𝑓
11		vp	. . . . . . . 8 setvar 𝑝
12	11	cv 1474	. . . . . . 7 class 𝑝
13	4	cv 1474	. . . . . . . 8 class 𝑎
14	5	cv 1474	. . . . . . . 8 class 𝑏
15		cwlkson 40798	. . . . . . . . 9 class WalksOn
16	6, 15	cfv 5804	. . . . . . . 8 class (WalksOn‘𝑔)
17	13, 14, 16	co 6549	. . . . . . 7 class (𝑎(WalksOn‘𝑔)𝑏)
18	10, 12, 17	wbr 4583	. . . . . 6 wff 𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝
19		ctrls 40899	. . . . . . . 8 class TrailS
20	6, 19	cfv 5804	. . . . . . 7 class (TrailS‘𝑔)
21	10, 12, 20	wbr 4583	. . . . . 6 wff 𝑓(TrailS‘𝑔)𝑝
22	18, 21	wa 383	. . . . 5 wff (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(TrailS‘𝑔)𝑝)
23	22, 9, 11	copab 4642	. . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(TrailS‘𝑔)𝑝)}
24	4, 5, 8, 8, 23	cmpt2 6551	. . 3 class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(TrailS‘𝑔)𝑝)})
25	2, 3, 24	cmpt 4643	. 2 class (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(TrailS‘𝑔)𝑝)}))
26	1, 25	wceq 1475	1 wff TrailsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(TrailS‘𝑔)𝑝)}))

This definition is referenced by:  trlsonfval  40913  trlsonprop  40915