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 e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> ( A e. V /\ B e. V /\ C e. V ) )

Proof

Step Hyp Ref Expression
1 wwlks2onv.v 
 |-  V = ( Vtx ` G )
2 1 wwlksonvtx 
 |-  ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) -> ( A e. V /\ C e. V ) )
3 2 adantl 
 |-  ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> ( A e. V /\ C e. V ) )
4 simprl 
 |-  ( ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) /\ ( A e. V /\ C e. V ) ) -> A e. V )
5 wwlknon 
 |-  ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> ( <" A B C "> e. ( 2 WWalksN G ) /\ ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) )
6 wwlknbp1 
 |-  ( <" A B C "> e. ( 2 WWalksN G ) -> ( 2 e. NN0 /\ <" A B C "> e. Word ( Vtx ` G ) /\ ( # ` <" A B C "> ) = ( 2 + 1 ) ) )
7 s3fv1 
 |-  ( B e. U -> ( <" A B C "> ` 1 ) = B )
8 7 eqcomd 
 |-  ( B e. U -> B = ( <" A B C "> ` 1 ) )
9 8 adantl 
 |-  ( ( <" A B C "> e. Word ( Vtx ` G ) /\ B e. U ) -> B = ( <" A B C "> ` 1 ) )
10 1 eqcomi 
 |-  ( Vtx ` G ) = V
11 10 wrdeqi 
 |-  Word ( Vtx ` G ) = Word V
12 11 eleq2i 
 |-  ( <" A B C "> e. Word ( Vtx ` G ) <-> <" A B C "> e. Word V )
13 12 biimpi 
 |-  ( <" A B C "> e. Word ( Vtx ` G ) -> <" A B C "> e. Word V )
14 1ex 
 |-  1 e. _V
15 14 tpid2 
 |-  1 e. { 0 , 1 , 2 }
16 s3len 
 |-  ( # ` <" A B C "> ) = 3
17 16 oveq2i 
 |-  ( 0 ..^ ( # ` <" A B C "> ) ) = ( 0 ..^ 3 )
18 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
19 17 18 eqtri 
 |-  ( 0 ..^ ( # ` <" A B C "> ) ) = { 0 , 1 , 2 }
20 15 19 eleqtrri 
 |-  1 e. ( 0 ..^ ( # ` <" A B C "> ) )
21 wrdsymbcl 
 |-  ( ( <" A B C "> e. Word V /\ 1 e. ( 0 ..^ ( # ` <" A B C "> ) ) ) -> ( <" A B C "> ` 1 ) e. V )
22 13 20 21 sylancl 
 |-  ( <" A B C "> e. Word ( Vtx ` G ) -> ( <" A B C "> ` 1 ) e. V )
23 22 adantr 
 |-  ( ( <" A B C "> e. Word ( Vtx ` G ) /\ B e. U ) -> ( <" A B C "> ` 1 ) e. V )
24 9 23 eqeltrd 
 |-  ( ( <" A B C "> e. Word ( Vtx ` G ) /\ B e. U ) -> B e. V )
25 24 ex 
 |-  ( <" A B C "> e. Word ( Vtx ` G ) -> ( B e. U -> B e. V ) )
26 25 3ad2ant2 
 |-  ( ( 2 e. NN0 /\ <" A B C "> e. Word ( Vtx ` G ) /\ ( # ` <" A B C "> ) = ( 2 + 1 ) ) -> ( B e. U -> B e. V ) )
27 6 26 syl 
 |-  ( <" A B C "> e. ( 2 WWalksN G ) -> ( B e. U -> B e. V ) )
28 27 3ad2ant1 
 |-  ( ( <" A B C "> e. ( 2 WWalksN G ) /\ ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) -> ( B e. U -> B e. V ) )
29 5 28 sylbi 
 |-  ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) -> ( B e. U -> B e. V ) )
30 29 impcom 
 |-  ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> B e. V )
31 30 adantr 
 |-  ( ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) /\ ( A e. V /\ C e. V ) ) -> B e. V )
32 simprr 
 |-  ( ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) /\ ( A e. V /\ C e. V ) ) -> C e. V )
33 4 31 32 3jca 
 |-  ( ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) /\ ( A e. V /\ C e. V ) ) -> ( A e. V /\ B e. V /\ C e. V ) )
34 3 33 mpdan 
 |-  ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> ( A e. V /\ B e. V /\ C e. V ) )