Metamath Proof Explorer

Theorem rusgrnumwwlks

Description: Induction step for rusgrnumwwlk . (Contributed by Alexander van der Vekens, 24-Aug-2018) (Revised by AV, 7-May-2021) (Proof shortened by AV, 27-May-2022)

Ref Expression
Hypotheses rusgrnumwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
rusgrnumwwlk.l ⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
Assertion rusgrnumwwlks ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) → ( 𝑃 𝐿 ( 𝑁 + 1 ) ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 rusgrnumwwlk.l ⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
3 simpr2 ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑃 ∈ 𝑉 )
4 simpr3 ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
5 1 2 rusgrnumwwlklem ⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 𝐿 𝑁 ) = ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
6 5 eqeq1d ⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ↔ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) )
7 3 4 6 syl2anc ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) ↔ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) )
8 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
9 8 wwlksnredwwlkn0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
10 9 ex ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
11 10 3ad2ant3 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
12 11 adantl ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
13 12 imp ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
14 13 rabbidva ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } )
15 14 adantr ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } )
16 15 fveq2d ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) )
17 simp2 ⊢ ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑦 ‘ 0 ) = 𝑃 )
18 17 pm4.71ri ⊢ ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( 𝑦 ‘ 0 ) = 𝑃 ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
19 18 a1i ⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) ∧ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ( ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( 𝑦 ‘ 0 ) = 𝑃 ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
20 19 rexbidva ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑦 ‘ 0 ) = 𝑃 ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
21 fveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
22 21 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ‘ 0 ) = 𝑃 ↔ ( 𝑦 ‘ 0 ) = 𝑃 ) )
23 22 rexrab ⊢ ( ∃ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑦 ‘ 0 ) = 𝑃 ∧ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
24 20 23 bitr4di ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ) → ( ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ∃ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
25 24 rabbidva ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } )
26 25 adantr ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } )
27 26 fveq2d ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) )
28 simplr1 ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → 𝑉 ∈ Fin )
29 1 eleq1i ⊢ ( 𝑉 ∈ Fin ↔ ( Vtx ‘ 𝐺 ) ∈ Fin )
30 29 biimpi ⊢ ( 𝑉 ∈ Fin → ( Vtx ‘ 𝐺 ) ∈ Fin )
31 eqid ⊢ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) = ( ( 𝑁 + 1 ) WWalksN 𝐺 )
32 eqid ⊢ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } = { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 }
33 31 8 32 hashwwlksnext ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = Σ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) )
34 28 30 33 3syl ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = Σ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) )
35 fveq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ‘ 0 ) = ( 𝑤 ‘ 0 ) )
36 35 eqeq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ‘ 0 ) = 𝑃 ↔ ( 𝑤 ‘ 0 ) = 𝑃 ) )
37 36 cbvrabv ⊢ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 }
38 37 sumeq1i ⊢ Σ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = Σ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } )
39 38 a1i ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → Σ 𝑦 ∈ { 𝑥 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑥 ‘ 0 ) = 𝑃 } ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = Σ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) )
40 27 34 39 3eqtrd ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ∃ 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = Σ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) )
41 rusgrnumwwlkslem ⊢ ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } )
42 41 eqcomd ⊢ ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } = { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } )
43 42 fveq2d ⊢ ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) )
44 43 adantl ⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) ∧ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) )
45 elrabi ⊢ ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) )
46 45 adantl ⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) ∧ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) → 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) )
47 1 8 wwlksnexthasheq ⊢ ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) )
48 46 47 syl ⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) ∧ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) )
49 1 rusgrpropadjvtx ⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
50 fveq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
51 50 eqeq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑦 ‘ 0 ) = 𝑃 ) )
52 51 elrab ⊢ ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ↔ ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) )
53 1 8 wwlknp ⊢ ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
54 53 adantr ⊢ ( ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) → ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
55 simpll ⊢ ( ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑦 ∈ Word 𝑉 )
56 nn0p1gt0 ⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 1 ) )
57 56 3ad2ant3 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 0 < ( 𝑁 + 1 ) )
58 57 adantl ⊢ ( ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 0 < ( 𝑁 + 1 ) )
59 breq2 ⊢ ( ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) → ( 0 < ( ♯ ‘ 𝑦 ) ↔ 0 < ( 𝑁 + 1 ) ) )
60 59 ad2antlr ⊢ ( ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 0 < ( ♯ ‘ 𝑦 ) ↔ 0 < ( 𝑁 + 1 ) ) )
61 58 60 mpbird ⊢ ( ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 0 < ( ♯ ‘ 𝑦 ) )
62 hashle00 ⊢ ( 𝑦 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑦 ) ≤ 0 ↔ 𝑦 = ∅ ) )
63 lencl ⊢ ( 𝑦 ∈ Word 𝑉 → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
64 63 nn0red ⊢ ( 𝑦 ∈ Word 𝑉 → ( ♯ ‘ 𝑦 ) ∈ ℝ )
65 0re ⊢ 0 ∈ ℝ
66 lenlt ⊢ ( ( ( ♯ ‘ 𝑦 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ♯ ‘ 𝑦 ) ≤ 0 ↔ ¬ 0 < ( ♯ ‘ 𝑦 ) ) )
67 66 bicomd ⊢ ( ( ( ♯ ‘ 𝑦 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ¬ 0 < ( ♯ ‘ 𝑦 ) ↔ ( ♯ ‘ 𝑦 ) ≤ 0 ) )
68 64 65 67 sylancl ⊢ ( 𝑦 ∈ Word 𝑉 → ( ¬ 0 < ( ♯ ‘ 𝑦 ) ↔ ( ♯ ‘ 𝑦 ) ≤ 0 ) )
69 nne ⊢ ( ¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅ )
70 69 a1i ⊢ ( 𝑦 ∈ Word 𝑉 → ( ¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅ ) )
71 62 68 70 3bitr4rd ⊢ ( 𝑦 ∈ Word 𝑉 → ( ¬ 𝑦 ≠ ∅ ↔ ¬ 0 < ( ♯ ‘ 𝑦 ) ) )
72 71 ad2antrr ⊢ ( ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ¬ 𝑦 ≠ ∅ ↔ ¬ 0 < ( ♯ ‘ 𝑦 ) ) )
73 72 con4bid ⊢ ( ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑦 ≠ ∅ ↔ 0 < ( ♯ ‘ 𝑦 ) ) )
74 61 73 mpbird ⊢ ( ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑦 ≠ ∅ )
75 55 74 jca ⊢ ( ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅ ) )
76 75 ex ⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ) → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅ ) ) )
77 76 3adant3 ⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑦 ) = ( 𝑁 + 1 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) { ( 𝑦 ‘ 𝑖 ) , ( 𝑦 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅ ) ) )
78 54 77 syl ⊢ ( ( 𝑦 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑦 ‘ 0 ) = 𝑃 ) → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅ ) ) )
79 52 78 sylbi ⊢ ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅ ) ) )
80 79 imp ⊢ ( ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅ ) )
81 lswcl ⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅ ) → ( lastS ‘ 𝑦 ) ∈ 𝑉 )
82 80 81 syl ⊢ ( ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( lastS ‘ 𝑦 ) ∈ 𝑉 )
83 82 ad2antrr ⊢ ( ( ( ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) ∧ ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) → ( lastS ‘ 𝑦 ) ∈ 𝑉 )
84 preq1 ⊢ ( 𝑝 = ( lastS ‘ 𝑦 ) → { 𝑝 , 𝑛 } = { ( lastS ‘ 𝑦 ) , 𝑛 } )
85 84 eleq1d ⊢ ( 𝑝 = ( lastS ‘ 𝑦 ) → ( { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) ↔ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) ) )
86 85 rabbidv ⊢ ( 𝑝 = ( lastS ‘ 𝑦 ) → { 𝑛 ∈ 𝑉 ∣ { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } = { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } )
87 86 fveqeq2d ⊢ ( 𝑝 = ( lastS ‘ 𝑦 ) → ( ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ↔ ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) )
88 87 rspcva ⊢ ( ( ( lastS ‘ 𝑦 ) ∈ 𝑉 ∧ ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) → ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 )
89 83 88 sylancom ⊢ ( ( ( ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) ∧ ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) → ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 )
90 89 exp41 ⊢ ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) → ( ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 → ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) ) ) )
91 90 com14 ⊢ ( ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) → ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) ) ) )
92 91 3ad2ant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑝 ∈ 𝑉 ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { 𝑝 , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) → ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) ) ) )
93 49 92 syl ⊢ ( 𝐺 RegUSGraph 𝐾 → ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) → ( 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } → ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 ) ) ) )
94 93 imp41 ⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) ∧ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) → ( ♯ ‘ { 𝑛 ∈ 𝑉 ∣ { ( lastS ‘ 𝑦 ) , 𝑛 } ∈ ( Edg ‘ 𝐺 ) } ) = 𝐾 )
95 44 48 94 3eqtrd ⊢ ( ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) ∧ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = 𝐾 )
96 95 sumeq2dv ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → Σ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = Σ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } 𝐾 )
97 oveq1 ⊢ ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) → ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) · 𝐾 ) = ( ( 𝐾 ↑ 𝑁 ) · 𝐾 ) )
98 97 adantl ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) · 𝐾 ) = ( ( 𝐾 ↑ 𝑁 ) · 𝐾 ) )
99 wwlksnfi ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
100 29 99 sylbi ⊢ ( 𝑉 ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
101 100 3ad2ant1 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
102 101 ad2antlr ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
103 rabfi ⊢ ( ( 𝑁 WWalksN 𝐺 ) ∈ Fin → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ∈ Fin )
104 102 103 syl ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ∈ Fin )
105 rusgrusgr ⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph )
106 simp1 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑉 ∈ Fin )
107 105 106 anim12i ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
108 1 isfusgr ⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
109 107 108 sylibr ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐺 ∈ FinUSGraph )
110 simpl ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐺 RegUSGraph 𝐾 )
111 ne0i ⊢ ( 𝑃 ∈ 𝑉 → 𝑉 ≠ ∅ )
112 111 3ad2ant2 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑉 ≠ ∅ )
113 112 adantl ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝑉 ≠ ∅ )
114 1 frusgrnn0 ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → 𝐾 ∈ ℕ0 )
115 109 110 113 114 syl3anc ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐾 ∈ ℕ0 )
116 115 nn0cnd ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → 𝐾 ∈ ℂ )
117 116 adantr ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → 𝐾 ∈ ℂ )
118 fsumconst ⊢ ( ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ∈ Fin ∧ 𝐾 ∈ ℂ ) → Σ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } 𝐾 = ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) · 𝐾 ) )
119 104 117 118 syl2anc ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → Σ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } 𝐾 = ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) · 𝐾 ) )
120 116 4 expp1d ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝐾 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐾 ↑ 𝑁 ) · 𝐾 ) )
121 120 adantr ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( 𝐾 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐾 ↑ 𝑁 ) · 𝐾 ) )
122 98 119 121 3eqtr4d ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → Σ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } 𝐾 = ( 𝐾 ↑ ( 𝑁 + 1 ) ) )
123 96 122 eqtrd ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → Σ 𝑦 ∈ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 + 1 ) ) = 𝑦 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( lastS ‘ 𝑦 ) , ( lastS ‘ 𝑤 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) )
124 16 40 123 3eqtrd ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) )
125 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
126 125 3ad2ant3 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℕ0 )
127 126 adantl ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑁 + 1 ) ∈ ℕ0 )
128 1 2 rusgrnumwwlklem ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( 𝑃 𝐿 ( 𝑁 + 1 ) ) = ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
129 128 eqeq1d ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( ( 𝑃 𝐿 ( 𝑁 + 1 ) ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) ↔ ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) ) )
130 3 127 129 syl2anc ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑃 𝐿 ( 𝑁 + 1 ) ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) ↔ ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) ) )
131 130 adantr ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( ( 𝑃 𝐿 ( 𝑁 + 1 ) ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) ↔ ( ♯ ‘ { 𝑤 ∈ ( ( 𝑁 + 1 ) WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) ) )
132 124 131 mpbird ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) ) → ( 𝑃 𝐿 ( 𝑁 + 1 ) ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) )
133 132 ex ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ♯ ‘ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( 𝐾 ↑ 𝑁 ) → ( 𝑃 𝐿 ( 𝑁 + 1 ) ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) ) )
134 7 133 sylbid ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ ( 𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑃 𝐿 𝑁 ) = ( 𝐾 ↑ 𝑁 ) → ( 𝑃 𝐿 ( 𝑁 + 1 ) ) = ( 𝐾 ↑ ( 𝑁 + 1 ) ) ) )