Metamath Proof Explorer

Theorem wwlksn0

Description: A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018) (Revised by AV, 9-Apr-2021) (Proof shortened by AV, 21-May-2021)

Ref Expression
Hypothesis wwlkssswrd.v ⊢ V = Vtx ⁡ G
Assertion wwlksn0 ⊢ W ∈ 0 WWalksN G → ∃ v ∈ V W = ⟨“ v ”⟩

Proof

Step Hyp Ref Expression
1 wwlkssswrd.v ⊢ V = Vtx ⁡ G
2 wrdl1exs1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 1 → ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩
3 fveqeq2 ⊢ w = W → w = 1 ↔ W = 1
4 wwlksn0s ⊢ 0 WWalksN G = w ∈ Word Vtx ⁡ G | w = 1
5 3 4 elrab2 ⊢ W ∈ 0 WWalksN G ↔ W ∈ Word Vtx ⁡ G ∧ W = 1
6 1 rexeqi ⊢ ∃ v ∈ V W = ⟨“ v ”⟩ ↔ ∃ v ∈ Vtx ⁡ G W = ⟨“ v ”⟩
7 2 5 6 3imtr4i ⊢ W ∈ 0 WWalksN G → ∃ v ∈ V W = ⟨“ v ”⟩