This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwlkson ⊢ WalksOn
1 vg ⊢ 𝑔
2 cvv ⊢ V
3 va ⊢ 𝑎
4 cvtx ⊢ Vtx
5 1 cv ⊢ 𝑔
6 5 4 cfv ⊢ ( Vtx ‘ 𝑔 )
7 vb ⊢ 𝑏
8 vf ⊢ 𝑓
9 vp ⊢ 𝑝
10 8 cv ⊢ 𝑓
11 cwlks ⊢ Walks
12 5 11 cfv ⊢ ( Walks ‘ 𝑔 )
13 9 cv ⊢ 𝑝
14 10 13 12 wbr ⊢ 𝑓 ( Walks ‘ 𝑔 ) 𝑝
15 cc0 ⊢ 0
16 15 13 cfv ⊢ ( 𝑝 ‘ 0 )
17 3 cv ⊢ 𝑎
18 16 17 wceq ⊢ ( 𝑝 ‘ 0 ) = 𝑎
19 chash ⊢ ♯
20 10 19 cfv ⊢ ( ♯ ‘ 𝑓 )
21 20 13 cfv ⊢ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) )
22 7 cv ⊢ 𝑏
23 21 22 wceq ⊢ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏
24 14 18 23 w3a ⊢ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 )
25 24 8 9 copab ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) }
26 3 7 6 6 25 cmpo ⊢ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } )
27 1 2 26 cmpt ⊢ ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) )
28 0 27 wceq ⊢ WalksOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) )