Definition df-wwlksnon

Description: Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 11-May-2021)

	Ref	Expression
Assertion	df-wwlksnon	⊢ WWalksNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwwlksnon	⊢ WWalksNOn
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vg	⊢ 𝑔
4		cvv	⊢ V
5		va	⊢ 𝑎
6		cvtx	⊢ Vtx
7	3	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( Vtx ‘ 𝑔 )
9		vb	⊢ 𝑏
10		vw	⊢ 𝑤
11	1	cv	⊢ 𝑛
12		cwwlksn	⊢ WWalksN
13	11 7 12	co	⊢ ( 𝑛 WWalksN 𝑔 )
14	10	cv	⊢ 𝑤
15		cc0	⊢ 0
16	15 14	cfv	⊢ ( 𝑤 ‘ 0 )
17	5	cv	⊢ 𝑎
18	16 17	wceq	⊢ ( 𝑤 ‘ 0 ) = 𝑎
19	11 14	cfv	⊢ ( 𝑤 ‘ 𝑛 )
20	9	cv	⊢ 𝑏
21	19 20	wceq	⊢ ( 𝑤 ‘ 𝑛 ) = 𝑏
22	18 21	wa	⊢ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 )
23	22 10 13	crab	⊢ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) }
24	5 9 8 8 23	cmpo	⊢ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } )
25	1 3 2 4 24	cmpo	⊢ ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) )
26	0 25	wceq	⊢ WWalksNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) )