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