Metamath Proof Explorer

Theorem wwlksnfi

Description: The number of walks represented by words of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 30-Jul-2018) (Revised by AV, 19-Apr-2021) (Proof shortened by JJ, 18-Nov-2022)

Ref Expression
Assertion wwlksnfi ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 wrdnfi ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ∈ Fin )
2 simpr ⊢ ( ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) → ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) )
3 2 rgenw ⊢ ∀ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ( ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) → ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) )
4 ss2rab ⊢ ( { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } ⊆ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } ↔ ∀ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ( ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) → ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) )
5 3 4 mpbir ⊢ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } ⊆ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) }
6 5 a1i ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } ⊆ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } )
7 1 6 ssfid ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } ∈ Fin )
8 wwlksn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } )
9 df-rab ⊢ { 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) } = { 𝑤 ∣ ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) }
10 8 9 eqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∣ ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } )
11 3anan12 ⊢ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
12 11 anbi1i ⊢ ( ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ↔ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) )
13 anass ⊢ ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ) )
14 12 13 bitri ⊢ ( ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ) )
15 14 abbii ⊢ { 𝑤 ∣ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } = { 𝑤 ∣ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ) }
16 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
17 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
18 16 17 iswwlks ⊢ ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
19 18 anbi1i ⊢ ( ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ↔ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) )
20 19 abbii ⊢ { 𝑤 ∣ ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } = { 𝑤 ∣ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) }
21 df-rab ⊢ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } = { 𝑤 ∣ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) ) }
22 15 20 21 3eqtr4i ⊢ { 𝑤 ∣ ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) }
23 10 22 eqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } )
24 23 eleq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 WWalksN 𝐺 ) ∈ Fin ↔ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) } ∈ Fin ) )
25 7 24 syl5ibr ⊢ ( 𝑁 ∈ ℕ0 → ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin ) )
26 df-nel ⊢ ( 𝑁 ∉ ℕ0 ↔ ¬ 𝑁 ∈ ℕ0 )
27 26 biimpri ⊢ ( ¬ 𝑁 ∈ ℕ0 → 𝑁 ∉ ℕ0 )
28 27 olcd ⊢ ( ¬ 𝑁 ∈ ℕ0 → ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ0 ) )
29 wwlksnndef ⊢ ( ( 𝐺 ∉ V ∨ 𝑁 ∉ ℕ0 ) → ( 𝑁 WWalksN 𝐺 ) = ∅ )
30 28 29 syl ⊢ ( ¬ 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = ∅ )
31 0fin ⊢ ∅ ∈ Fin
32 30 31 eqeltrdi ⊢ ( ¬ 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )
33 32 a1d ⊢ ( ¬ 𝑁 ∈ ℕ0 → ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin ) )
34 25 33 pm2.61i ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑁 WWalksN 𝐺 ) ∈ Fin )