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

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