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 ⊢ V = Vtx ⁡ G
Assertion elwwlks2ons3 ⊢ W ∈ A 2 WWalksNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C

Proof

Step Hyp Ref Expression
1 wwlks2onv.v ⊢ V = Vtx ⁡ G
2 id ⊢ W ∈ A 2 WWalksNOn G C → W ∈ A 2 WWalksNOn G C
3 1 elwwlks2ons3im ⊢ W ∈ A 2 WWalksNOn G C → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
4 anass ⊢ W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V ↔ W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
5 2 3 4 sylanbrc ⊢ W ∈ A 2 WWalksNOn G C → W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V
6 simpr ⊢ W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V → W ⁡ 1 ∈ V
7 s3eq2 ⊢ b = W ⁡ 1 → ⟨“ AbC ”⟩ = ⟨“ A W ⁡ 1 C ”⟩
8 eqeq2 ⊢ ⟨“ AbC ”⟩ = ⟨“ A W ⁡ 1 C ”⟩ → W = ⟨“ AbC ”⟩ ↔ W = ⟨“ A W ⁡ 1 C ”⟩
9 eleq1 ⊢ ⟨“ AbC ”⟩ = ⟨“ A W ⁡ 1 C ”⟩ → ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ ⟨“ A W ⁡ 1 C ”⟩ ∈ A 2 WWalksNOn G C
10 8 9 anbi12d ⊢ ⟨“ AbC ”⟩ = ⟨“ A W ⁡ 1 C ”⟩ → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ ⟨“ A W ⁡ 1 C ”⟩ ∈ A 2 WWalksNOn G C
11 7 10 syl ⊢ b = W ⁡ 1 → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ ⟨“ A W ⁡ 1 C ”⟩ ∈ A 2 WWalksNOn G C
12 11 adantl ⊢ W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V ∧ b = W ⁡ 1 → W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ ⟨“ A W ⁡ 1 C ”⟩ ∈ A 2 WWalksNOn G C
13 simpr ⊢ W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ → W = ⟨“ A W ⁡ 1 C ”⟩
14 eleq1 ⊢ W = ⟨“ A W ⁡ 1 C ”⟩ → W ∈ A 2 WWalksNOn G C ↔ ⟨“ A W ⁡ 1 C ”⟩ ∈ A 2 WWalksNOn G C
15 14 biimpac ⊢ W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ → ⟨“ A W ⁡ 1 C ”⟩ ∈ A 2 WWalksNOn G C
16 13 15 jca ⊢ W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ ⟨“ A W ⁡ 1 C ”⟩ ∈ A 2 WWalksNOn G C
17 16 adantr ⊢ W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V → W = ⟨“ A W ⁡ 1 C ”⟩ ∧ ⟨“ A W ⁡ 1 C ”⟩ ∈ A 2 WWalksNOn G C
18 6 12 17 rspcedvd ⊢ W ∈ A 2 WWalksNOn G C ∧ W = ⟨“ A W ⁡ 1 C ”⟩ ∧ W ⁡ 1 ∈ V → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C
19 5 18 syl ⊢ W ∈ A 2 WWalksNOn G C → ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C
20 eleq1 ⊢ ⟨“ AbC ”⟩ = W → ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ W ∈ A 2 WWalksNOn G C
21 20 eqcoms ⊢ W = ⟨“ AbC ”⟩ → ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C ↔ W ∈ A 2 WWalksNOn G C
22 21 biimpa ⊢ W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C → W ∈ A 2 WWalksNOn G C
23 22 rexlimivw ⊢ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C → W ∈ A 2 WWalksNOn G C
24 19 23 impbii ⊢ W ∈ A 2 WWalksNOn G C ↔ ∃ b ∈ V W = ⟨“ AbC ”⟩ ∧ ⟨“ AbC ”⟩ ∈ A 2 WWalksNOn G C