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 ‘ 𝑔 ) 𝑏 ) 𝑤 } ) )