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∈A2WWalksNOnGC↔∃b∈VW=⟨“AbC”⟩∧⟨“AbC”⟩∈A2WWalksNOnGC

Proof

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