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

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion elwwlks2s3 ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )

Proof

Step Hyp Ref Expression
1 elwwlks2s3.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wwlknbp1 ⊢ ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) → ( 2 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 2 + 1 ) ) )
3 1 wrdeqi ⊢ Word 𝑉 = Word ( Vtx ‘ 𝐺 )
4 3 eleq2i ⊢ ( 𝑊 ∈ Word 𝑉 ↔ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
5 df-3 ⊢ 3 = ( 2 + 1 )
6 5 eqeq2i ⊢ ( ( ♯ ‘ 𝑊 ) = 3 ↔ ( ♯ ‘ 𝑊 ) = ( 2 + 1 ) )
7 4 6 anbi12i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) ↔ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 2 + 1 ) ) )
8 wrdl3s3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
9 7 8 sylbb1 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 2 + 1 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
10 9 3adant1 ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 2 + 1 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
11 2 10 syl ⊢ ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )