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 ) = 𝑏 )