Metamath Proof Explorer

Theorem wwlks2onv

Description: If a length 3 string represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018) (Proof shortened by AV, 14-Mar-2022)

Ref Expression
Hypothesis wwlks2onv.v ⊢V=Vtx⁡G
Assertion wwlks2onv ⊢B∈U∧⟨“ABC”⟩∈A2WWalksNOnGC→A∈V∧B∈V∧C∈V

Proof

Step Hyp Ref Expression
1 wwlks2onv.v ⊢V=Vtx⁡G
2 1 wwlksonvtx ⊢⟨“ABC”⟩∈A2WWalksNOnGC→A∈V∧C∈V
3 2 adantl ⊢B∈U∧⟨“ABC”⟩∈A2WWalksNOnGC→A∈V∧C∈V
4 simprl ⊢B∈U∧⟨“ABC”⟩∈A2WWalksNOnGC∧A∈V∧C∈V→A∈V
5 wwlknon ⊢⟨“ABC”⟩∈A2WWalksNOnGC↔⟨“ABC”⟩∈2WWalksNG∧⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C
6 wwlknbp1 ⊢⟨“ABC”⟩∈2WWalksNG→2∈ℕ0∧⟨“ABC”⟩∈WordVtx⁡G∧⟨“ABC”⟩=2+1
7 s3fv1 ⊢B∈U→⟨“ABC”⟩⁡1=B
8 7 eqcomd ⊢B∈U→B=⟨“ABC”⟩⁡1
9 8 adantl ⊢⟨“ABC”⟩∈WordVtx⁡G∧B∈U→B=⟨“ABC”⟩⁡1
10 1 eqcomi ⊢Vtx⁡G=V
11 10 wrdeqi ⊢WordVtx⁡G=WordV
12 11 eleq2i ⊢⟨“ABC”⟩∈WordVtx⁡G↔⟨“ABC”⟩∈WordV
13 12 biimpi ⊢⟨“ABC”⟩∈WordVtx⁡G→⟨“ABC”⟩∈WordV
14 1ex ⊢1∈V
15 14 tpid2 ⊢1∈012
16 s3len ⊢⟨“ABC”⟩=3
17 16 oveq2i ⊢0..^⟨“ABC”⟩=0..^3
18 fzo0to3tp ⊢0..^3=012
19 17 18 eqtri ⊢0..^⟨“ABC”⟩=012
20 15 19 eleqtrri ⊢1∈0..^⟨“ABC”⟩
21 wrdsymbcl ⊢⟨“ABC”⟩∈WordV∧1∈0..^⟨“ABC”⟩→⟨“ABC”⟩⁡1∈V
22 13 20 21 sylancl ⊢⟨“ABC”⟩∈WordVtx⁡G→⟨“ABC”⟩⁡1∈V
23 22 adantr ⊢⟨“ABC”⟩∈WordVtx⁡G∧B∈U→⟨“ABC”⟩⁡1∈V
24 9 23 eqeltrd ⊢⟨“ABC”⟩∈WordVtx⁡G∧B∈U→B∈V
25 24 ex ⊢⟨“ABC”⟩∈WordVtx⁡G→B∈U→B∈V
26 25 3ad2ant2 ⊢2∈ℕ0∧⟨“ABC”⟩∈WordVtx⁡G∧⟨“ABC”⟩=2+1→B∈U→B∈V
27 6 26 syl ⊢⟨“ABC”⟩∈2WWalksNG→B∈U→B∈V
28 27 3ad2ant1 ⊢⟨“ABC”⟩∈2WWalksNG∧⟨“ABC”⟩⁡0=A∧⟨“ABC”⟩⁡2=C→B∈U→B∈V
29 5 28 sylbi ⊢⟨“ABC”⟩∈A2WWalksNOnGC→B∈U→B∈V
30 29 impcom ⊢B∈U∧⟨“ABC”⟩∈A2WWalksNOnGC→B∈V
31 30 adantr ⊢B∈U∧⟨“ABC”⟩∈A2WWalksNOnGC∧A∈V∧C∈V→B∈V
32 simprr ⊢B∈U∧⟨“ABC”⟩∈A2WWalksNOnGC∧A∈V∧C∈V→C∈V
33 4 31 32 3jca ⊢B∈U∧⟨“ABC”⟩∈A2WWalksNOnGC∧A∈V∧C∈V→A∈V∧B∈V∧C∈V
34 3 33 mpdan ⊢B∈U∧⟨“ABC”⟩∈A2WWalksNOnGC→A∈V∧B∈V∧C∈V