Metamath Proof Explorer


Theorem wlkn0

Description: The sequence of vertices of a walk cannot be empty, i.e. a walk always consists of at least one vertex. (Contributed by Alexander van der Vekens, 19-Jul-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Assertion wlkn0 ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝑃 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 wlkp ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
3 fdm ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → dom 𝑃 = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
4 3 eqcomd ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( 0 ... ( ♯ ‘ 𝐹 ) ) = dom 𝑃 )
5 2 4 syl ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = dom 𝑃 )
6 wlkcl ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
7 elnn0uz ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ( ℤ ‘ 0 ) )
8 fzn0 ( ( 0 ... ( ♯ ‘ 𝐹 ) ) ≠ ∅ ↔ ( ♯ ‘ 𝐹 ) ∈ ( ℤ ‘ 0 ) )
9 7 8 sylbb2 ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 0 ... ( ♯ ‘ 𝐹 ) ) ≠ ∅ )
10 6 9 syl ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 0 ... ( ♯ ‘ 𝐹 ) ) ≠ ∅ )
11 5 10 eqnetrrd ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → dom 𝑃 ≠ ∅ )
12 frel ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → Rel 𝑃 )
13 2 12 syl ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → Rel 𝑃 )
14 reldm0 ( Rel 𝑃 → ( 𝑃 = ∅ ↔ dom 𝑃 = ∅ ) )
15 14 necon3bid ( Rel 𝑃 → ( 𝑃 ≠ ∅ ↔ dom 𝑃 ≠ ∅ ) )
16 13 15 syl ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ≠ ∅ ↔ dom 𝑃 ≠ ∅ ) )
17 11 16 mpbird ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝑃 ≠ ∅ )