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

Metamath Proof Explorer

Theorem is0wlk

Description: A pair of an empty set (of edges) and a sequence of one vertex is a walk (of length 0). (Contributed by AV, 3-Jan-2021) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0wlk.v ⊢ V = Vtx ⁡ G
Assertion is0wlk ⊢ P = 0 N ∧ N ∈ V → ∅ Walks ⁡ G P

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ V = Vtx ⁡ G
2 1fv ⊢ N ∈ V ∧ P = 0 N → P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N
3 2 ancoms ⊢ P = 0 N ∧ N ∈ V → P : 0 … 0 ⟶ V ∧ P ⁡ 0 = N
4 3 simpld ⊢ P = 0 N ∧ N ∈ V → P : 0 … 0 ⟶ V
5 1 1vgrex ⊢ N ∈ V → G ∈ V
6 5 adantl ⊢ P = 0 N ∧ N ∈ V → G ∈ V
7 1 0wlk ⊢ G ∈ V → ∅ Walks ⁡ G P ↔ P : 0 … 0 ⟶ V
8 6 7 syl ⊢ P = 0 N ∧ N ∈ V → ∅ Walks ⁡ G P ↔ P : 0 … 0 ⟶ V
9 4 8 mpbird ⊢ P = 0 N ∧ N ∈ V → ∅ Walks ⁡ G P