Metamath Proof Explorer


Theorem elwwlks2ons3

Description: For each walk of length 2 between two vertices, there is a third vertex in the middle of the walk. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypothesis wwlks2onv.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion elwwlks2ons3 ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 wwlks2onv.v 𝑉 = ( Vtx ‘ 𝐺 )
2 id ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) )
3 1 elwwlks2ons3im ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) )
4 anass ( ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) ↔ ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) ) )
5 2 3 4 sylanbrc ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) )
6 simpr ( ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) → ( 𝑊 ‘ 1 ) ∈ 𝑉 )
7 s3eq2 ( 𝑏 = ( 𝑊 ‘ 1 ) → ⟨“ 𝐴 𝑏 𝐶 ”⟩ = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ )
8 eqeq2 ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ → ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ↔ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) )
9 eleq1 ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ → ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
10 8 9 anbi12d ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ → ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ↔ ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) )
11 7 10 syl ( 𝑏 = ( 𝑊 ‘ 1 ) → ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ↔ ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) )
12 11 adantl ( ( ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) ∧ 𝑏 = ( 𝑊 ‘ 1 ) ) → ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ↔ ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ) )
13 simpr ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) → 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ )
14 eleq1 ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ → ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
15 14 biimpac ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) → ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) )
16 13 15 jca ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
17 16 adantr ( ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) → ( 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∧ ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
18 6 12 17 rspcedvd ( ( ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ∧ 𝑊 = ⟨“ 𝐴 ( 𝑊 ‘ 1 ) 𝐶 ”⟩ ) ∧ ( 𝑊 ‘ 1 ) ∈ 𝑉 ) → ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
19 5 18 syl ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
20 eleq1 ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ = 𝑊 → ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
21 20 eqcoms ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ → ( ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )
22 21 biimpa ( ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) )
23 22 rexlimivw ( ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) )
24 19 23 impbii ( 𝑊 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ∃ 𝑏𝑉 ( 𝑊 = ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∧ ⟨“ 𝐴 𝑏 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) )