Metamath Proof Explorer

Theorem elwwlks2s3

Description: A walk of length 2 as word is a length 3 string. (Contributed by AV, 18-May-2021)

Ref Expression
Hypothesis elwwlks2s3.v ⊢ V = Vtx ⁡ G
Assertion elwwlks2s3 ⊢ W ∈ 2 WWalksN G → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩

Proof

Step Hyp Ref Expression
1 elwwlks2s3.v ⊢ V = Vtx ⁡ G
2 wwlknbp1 ⊢ W ∈ 2 WWalksN G → 2 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = 2 + 1
3 1 wrdeqi ⊢ Word V = Word Vtx ⁡ G
4 3 eleq2i ⊢ W ∈ Word V ↔ W ∈ Word Vtx ⁡ G
5 df-3 ⊢ 3 = 2 + 1
6 5 eqeq2i ⊢ W = 3 ↔ W = 2 + 1
7 4 6 anbi12i ⊢ W ∈ Word V ∧ W = 3 ↔ W ∈ Word Vtx ⁡ G ∧ W = 2 + 1
8 wrdl3s3 ⊢ W ∈ Word V ∧ W = 3 ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩
9 7 8 sylbb1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 2 + 1 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩
10 9 3adant1 ⊢ 2 ∈ ℕ 0 ∧ W ∈ Word Vtx ⁡ G ∧ W = 2 + 1 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩
11 2 10 syl ⊢ W ∈ 2 WWalksN G → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V W = ⟨“ abc ”⟩