Metamath Proof Explorer

Definition df-pthson

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) (Revised by AV, 9-Jan-2021)

Ref Expression
Assertion df-pthson ⊢ PathsOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a TrailsOn ⁡ g b p ∧ f Paths ⁡ g p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpthson class PathsOn
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 ctrlson class TrailsOn
13 5 12 cfv class TrailsOn ⁡ g
14 7 cv setvar b
15 11 14 13 co class a TrailsOn ⁡ g b
16 9 cv setvar p
17 10 16 15 wbr wff f a TrailsOn ⁡ g b p
18 cpths class Paths
19 5 18 cfv class Paths ⁡ g
20 10 16 19 wbr wff f Paths ⁡ g p
21 17 20 wa wff f a TrailsOn ⁡ g b p ∧ f Paths ⁡ g p
22 21 8 9 copab class f p | f a TrailsOn ⁡ g b p ∧ f Paths ⁡ g p
23 3 7 6 6 22 cmpo class a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a TrailsOn ⁡ g b p ∧ f Paths ⁡ g p
24 1 2 23 cmpt class g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a TrailsOn ⁡ g b p ∧ f Paths ⁡ g p
25 0 24 wceq wff PathsOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a TrailsOn ⁡ g b p ∧ f Paths ⁡ g p