Metamath Proof Explorer

Definition df-spthson

Description: Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 9-Jan-2021)

Ref Expression
Assertion df-spthson ⊢ SPathsOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a TrailsOn ⁡ g b p ∧ f SPaths ⁡ g p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cspthson class SPathsOn
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 cspths class SPaths
19 5 18 cfv class SPaths ⁡ g
20 10 16 19 wbr wff f SPaths ⁡ g p
21 17 20 wa wff f a TrailsOn ⁡ g b p ∧ f SPaths ⁡ g p
22 21 8 9 copab class f p | f a TrailsOn ⁡ g b p ∧ f SPaths ⁡ 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 SPaths ⁡ 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 SPaths ⁡ g p
25 0 24 wceq wff SPathsOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f a TrailsOn ⁡ g b p ∧ f SPaths ⁡ g p