Metamath Proof Explorer

Definition df-trlson

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)

Ref Expression
Assertion df-trlson ⊢ TrailsOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a WalksOn ⁡ g b p ∧ f Trails ⁡ g p

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrlson class TrailsOn
1 vg setvar g
2 cvv class V
3 va setvar a
4 cvtx class Vtx
5 1 cv setvar g
6 5 4 cfv class Vtx ⁡ g
7 vb setvar b
8 vf setvar f
9 vp setvar p
10 8 cv setvar f
11 3 cv setvar a
12 cwlkson class WalksOn
13 5 12 cfv class WalksOn ⁡ g
14 7 cv setvar b
15 11 14 13 co class a WalksOn ⁡ g b
16 9 cv setvar p
17 10 16 15 wbr wff f a WalksOn ⁡ g b p
18 ctrls class Trails
19 5 18 cfv class Trails ⁡ g
20 10 16 19 wbr wff f Trails ⁡ g p
21 17 20 wa wff f a WalksOn ⁡ g b p ∧ f Trails ⁡ g p
22 21 8 9 copab class f p | f a WalksOn ⁡ g b p ∧ f Trails ⁡ g p
23 3 7 6 6 22 cmpo class a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a WalksOn ⁡ g b p ∧ f Trails ⁡ g p
24 1 2 23 cmpt class g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a WalksOn ⁡ g b p ∧ f Trails ⁡ g p
25 0 24 wceq wff TrailsOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a WalksOn ⁡ g b p ∧ f Trails ⁡ g p