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