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 𝐺 ) 𝐶 ) ) )