Metamath Proof Explorer


Definition df-wspthsnon

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

Ref Expression
Assertion df-wspthsnon WSPathsNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwspthsnon WSPathsNOn
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 5 cv 𝑎
12 1 cv 𝑛
13 cwwlksnon WWalksNOn
14 12 7 13 co ( 𝑛 WWalksNOn 𝑔 )
15 9 cv 𝑏
16 11 15 14 co ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 )
17 vf 𝑓
18 17 cv 𝑓
19 cspthson SPathsOn
20 7 19 cfv ( SPathsOn ‘ 𝑔 )
21 11 15 20 co ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 )
22 10 cv 𝑤
23 18 22 21 wbr 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤
24 23 17 wex 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤
25 24 10 16 crab { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 }
26 5 9 8 8 25 cmpo ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } )
27 1 3 2 4 26 cmpo ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) )
28 0 27 wceq WSPathsNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) )