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

Metamath Proof Explorer

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 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) )