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 𝐺 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )