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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion is0wlk ( ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ∧ 𝑁 ∈ 𝑉 ) → ∅ ( Walks ‘ 𝐺 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1fv ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ) → ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) )
3 2 ancoms ⊢ ( ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ∧ 𝑁 ∈ 𝑉 ) → ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) )
4 3 simpld ⊢ ( ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ∧ 𝑁 ∈ 𝑉 ) → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 )
5 1 1vgrex ⊢ ( 𝑁 ∈ 𝑉 → 𝐺 ∈ V )
6 5 adantl ⊢ ( ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ∧ 𝑁 ∈ 𝑉 ) → 𝐺 ∈ V )
7 1 0wlk ⊢ ( 𝐺 ∈ V → ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
8 6 7 syl ⊢ ( ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ∧ 𝑁 ∈ 𝑉 ) → ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
9 4 8 mpbird ⊢ ( ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ∧ 𝑁 ∈ 𝑉 ) → ∅ ( Walks ‘ 𝐺 ) 𝑃 )