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 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) )