Metamath Proof Explorer

Theorem s3wwlks2on

Description: A length 3 string which represents a walk of length 2 between two vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021)

Ref Expression
Hypothesis s3wwlks2on.v ⊢V=Vtx⁡G
Assertion s3wwlks2on ⊢G∈UPGraph∧A∈V∧C∈V→⟨“ABC”⟩∈A2WWalksNOnGC↔∃ffWalks⁡G⟨“ABC”⟩∧f=2

Proof

Step Hyp Ref Expression
1 s3wwlks2on.v ⊢V=Vtx⁡G
2 wwlknon ⊢⟨“ABC”⟩∈A2WWalksNOnGC↔⟨“ABC”⟩∈2WWalksNG∧⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C
3 2 a1i ⊢G∈UPGraph∧A∈V∧C∈V→⟨“ABC”⟩∈A2WWalksNOnGC↔⟨“ABC”⟩∈2WWalksNG∧⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C
4 3anass ⊢⟨“ABC”⟩∈2WWalksNG∧⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C↔⟨“ABC”⟩∈2WWalksNG∧⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C
5 s3fv0 ⊢A∈V→⟨“ABC”⟩⁡0=A
6 s3fv2 ⊢C∈V→⟨“ABC”⟩⁡2=C
7 5 6 anim12i ⊢A∈V∧C∈V→⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C
8 7 3adant1 ⊢G∈UPGraph∧A∈V∧C∈V→⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C
9 8 biantrud ⊢G∈UPGraph∧A∈V∧C∈V→⟨“ABC”⟩∈2WWalksNG↔⟨“ABC”⟩∈2WWalksNG∧⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C
10 4 9 bitr4id ⊢G∈UPGraph∧A∈V∧C∈V→⟨“ABC”⟩∈2WWalksNG∧⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C↔⟨“ABC”⟩∈2WWalksNG
11 wlklnwwlknupgr ⊢G∈UPGraph→∃ffWalks⁡G⟨“ABC”⟩∧f=2↔⟨“ABC”⟩∈2WWalksNG
12 11 bicomd ⊢G∈UPGraph→⟨“ABC”⟩∈2WWalksNG↔∃ffWalks⁡G⟨“ABC”⟩∧f=2
13 12 3ad2ant1 ⊢G∈UPGraph∧A∈V∧C∈V→⟨“ABC”⟩∈2WWalksNG↔∃ffWalks⁡G⟨“ABC”⟩∧f=2
14 3 10 13 3bitrd ⊢G∈UPGraph∧A∈V∧C∈V→⟨“ABC”⟩∈A2WWalksNOnGC↔∃ffWalks⁡G⟨“ABC”⟩∧f=2