This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 ) 𝑃 → 𝑃 ≠ ∅ )