Metamath Proof Explorer

Theorem ewlksfval

Description: The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion ewlksfval ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( 𝐺 EdgWalks 𝑆 ) = { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 ewlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 df-ewlks ⊢ EdgWalks = ( 𝑔 ∈ V , 𝑠 ∈ ℕ0* ↦ { 𝑓 ∣ [ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )
3 2 a1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → EdgWalks = ( 𝑔 ∈ V , 𝑠 ∈ ℕ0* ↦ { 𝑓 ∣ [ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ) )
4 fvexd ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( iEdg ‘ 𝑔 ) ∈ V )
5 simpr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → 𝑖 = ( iEdg ‘ 𝑔 ) )
6 fveq2 ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
7 6 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
8 7 adantr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
9 5 8 eqtrd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → 𝑖 = ( iEdg ‘ 𝐺 ) )
10 9 dmeqd ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → dom 𝑖 = dom ( iEdg ‘ 𝐺 ) )
11 wrdeq ⊢ ( dom 𝑖 = dom ( iEdg ‘ 𝐺 ) → Word dom 𝑖 = Word dom ( iEdg ‘ 𝐺 ) )
12 10 11 syl ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → Word dom 𝑖 = Word dom ( iEdg ‘ 𝐺 ) )
13 12 eleq2d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → ( 𝑓 ∈ Word dom 𝑖 ↔ 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ) )
14 simpr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
15 14 adantr ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → 𝑠 = 𝑆 )
16 9 fveq1d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) )
17 9 fveq1d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) )
18 16 17 ineq12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) = ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) )
19 18 fveq2d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) = ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) )
20 15 19 breq12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → ( 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) )
21 20 ralbidv ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) )
22 13 21 anbi12d ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ∧ 𝑖 = ( iEdg ‘ 𝑔 ) ) → ( ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) ↔ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) ) )
23 4 22 sbcied ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → ( [ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) ↔ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) ) )
24 23 abbidv ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) → { 𝑓 ∣ [ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } = { 𝑓 ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )
25 24 adantl ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → { 𝑓 ∣ [ ( iEdg ‘ 𝑔 ) / 𝑖 ] ( 𝑓 ∈ Word dom 𝑖 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑠 ≤ ( ♯ ‘ ( ( 𝑖 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝑖 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } = { 𝑓 ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )
26 elex ⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
27 26 adantr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → 𝐺 ∈ V )
28 simpr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → 𝑆 ∈ ℕ0* )
29 df-rab ⊢ { 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } = { 𝑓 ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) }
30 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
31 30 dmex ⊢ dom ( iEdg ‘ 𝐺 ) ∈ V
32 31 wrdexi ⊢ Word dom ( iEdg ‘ 𝐺 ) ∈ V
33 32 rabex ⊢ { 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ∈ V
34 33 a1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → { 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ∈ V )
35 29 34 eqeltrrid ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → { 𝑓 ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ∈ V )
36 3 25 27 28 35 ovmpod ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( 𝐺 EdgWalks 𝑆 ) = { 𝑓 ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )
37 1 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐼
38 37 a1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( iEdg ‘ 𝐺 ) = 𝐼 )
39 38 dmeqd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → dom ( iEdg ‘ 𝐺 ) = dom 𝐼 )
40 wrdeq ⊢ ( dom ( iEdg ‘ 𝐺 ) = dom 𝐼 → Word dom ( iEdg ‘ 𝐺 ) = Word dom 𝐼 )
41 39 40 syl ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → Word dom ( iEdg ‘ 𝐺 ) = Word dom 𝐼 )
42 41 eleq2d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ↔ 𝑓 ∈ Word dom 𝐼 ) )
43 38 fveq1d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) = ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) )
44 38 fveq1d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) )
45 43 44 ineq12d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) = ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) )
46 45 fveq2d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) = ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) )
47 46 breq2d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) )
48 47 ralbidv ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) )
49 42 48 anbi12d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) ↔ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) ) )
50 49 abbidv ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → { 𝑓 ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } = { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )
51 36 50 eqtrd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( 𝐺 EdgWalks 𝑆 ) = { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )