Metamath Proof Explorer

Definition df-wlkson

Description: Define the collection of walks with particular endpoints (in a hypergraph). The predicate F ( A ( WalksOnG ) B ) P can be read as "The pair <. F , P >. represents a walk from vertex A to vertex B in a graph G ", see also iswlkon . This corresponds to the "x0-x(l)-walks", see Definition in Bollobas p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017) (Revised by AV, 28-Dec-2020)

Ref Expression
Assertion df-wlkson ⊢ WalksOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f Walks ⁡ g p ∧ p ⁡ 0 = a ∧ p ⁡ f = b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwlkson class WalksOn
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 cwlks class Walks
12 5 11 cfv class Walks ⁡ g
13 9 cv setvar p
14 10 13 12 wbr wff f Walks ⁡ g p
15 cc0 class 0
16 15 13 cfv class p ⁡ 0
17 3 cv setvar a
18 16 17 wceq wff p ⁡ 0 = a
19 chash class .
20 10 19 cfv class f
21 20 13 cfv class p ⁡ f
22 7 cv setvar b
23 21 22 wceq wff p ⁡ f = b
24 14 18 23 w3a wff f Walks ⁡ g p ∧ p ⁡ 0 = a ∧ p ⁡ f = b
25 24 8 9 copab class f p | f Walks ⁡ g p ∧ p ⁡ 0 = a ∧ p ⁡ f = b
26 3 7 6 6 25 cmpo class a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f Walks ⁡ g p ∧ p ⁡ 0 = a ∧ p ⁡ f = b
27 1 2 26 cmpt class g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f Walks ⁡ g p ∧ p ⁡ 0 = a ∧ p ⁡ f = b
28 0 27 wceq wff WalksOn = g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ f p | f Walks ⁡ g p ∧ p ⁡ 0 = a ∧ p ⁡ f = b