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