This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Walks, paths and cycles Walks as words df-wspthsn
Description: Define the collection of simple paths of a fixed length 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-wspthsn ⊢ WSPathsN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 } )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cwwspthsn ⊢ WSPathsN
1
vn ⊢ 𝑛
2
cn0 ⊢ ℕ0
3
vg ⊢ 𝑔
4
cvv ⊢ V
5
vw ⊢ 𝑤
6
1
cv ⊢ 𝑛
7
cwwlksn ⊢ WWalksN
8
3
cv ⊢ 𝑔
9
6 8 7
co ⊢ ( 𝑛 WWalksN 𝑔 )
10
vf ⊢ 𝑓
11
10
cv ⊢ 𝑓
12
cspths ⊢ SPaths
13
8 12
cfv ⊢ ( SPaths ‘ 𝑔 )
14
5
cv ⊢ 𝑤
15
11 14 13
wbr ⊢ 𝑓 ( SPaths ‘ 𝑔 ) 𝑤
16
15 10
wex ⊢ ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤
17
16 5 9
crab ⊢ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 }
18
1 3 2 4 17
cmpo ⊢ ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 } )
19
0 18
wceq ⊢ WSPathsN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 } )