Metamath Proof Explorer


Theorem midwwlks2s3

Description: There is a vertex between the endpoints of a walk of length 2 between two vertices as length 3 string. (Contributed by AV, 10-Jan-2022)

Ref Expression
Hypothesis elwwlks2s3.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion midwwlks2s3 ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) → ∃ 𝑏𝑉 ( 𝑊 ‘ 1 ) = 𝑏 )

Proof

Step Hyp Ref Expression
1 elwwlks2s3.v 𝑉 = ( Vtx ‘ 𝐺 )
2 1 elwwlks2s3 ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ )
3 fveq1 ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑊 ‘ 1 ) = ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 1 ) )
4 s3fv1 ( 𝑏𝑉 → ( ⟨“ 𝑎 𝑏 𝑐 ”⟩ ‘ 1 ) = 𝑏 )
5 3 4 sylan9eqr ( ( 𝑏𝑉𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ ) → ( 𝑊 ‘ 1 ) = 𝑏 )
6 5 ex ( 𝑏𝑉 → ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑊 ‘ 1 ) = 𝑏 ) )
7 6 adantl ( ( 𝑎𝑉𝑏𝑉 ) → ( 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑊 ‘ 1 ) = 𝑏 ) )
8 7 rexlimdvw ( ( 𝑎𝑉𝑏𝑉 ) → ( ∃ 𝑐𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ( 𝑊 ‘ 1 ) = 𝑏 ) )
9 8 reximdva ( 𝑎𝑉 → ( ∃ 𝑏𝑉𝑐𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ∃ 𝑏𝑉 ( 𝑊 ‘ 1 ) = 𝑏 ) )
10 9 rexlimiv ( ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 𝑊 = ⟨“ 𝑎 𝑏 𝑐 ”⟩ → ∃ 𝑏𝑉 ( 𝑊 ‘ 1 ) = 𝑏 )
11 2 10 syl ( 𝑊 ∈ ( 2 WWalksN 𝐺 ) → ∃ 𝑏𝑉 ( 𝑊 ‘ 1 ) = 𝑏 )