This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrwwlks2on

Description: A walk of length 2 between two vertices as word in a simple graph. This theorem is analogous to umgrwwlks2on except it talks about simple graphs and therefore does not require the Axiom of Choice for its proof. (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses s3wwlks2on.v 
|- V = ( Vtx ` G )
usgrwwlks2on.e 
|- E = ( Edg ` G )
Assertion usgrwwlks2on 
|- ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> ( { A , B } e. E /\ { B , C } e. E ) ) )

Proof

Step Hyp Ref Expression
1 s3wwlks2on.v 
 |-  V = ( Vtx ` G )
2 usgrwwlks2on.e 
 |-  E = ( Edg ` G )
3 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
4 3 adantr 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> G e. USPGraph )
5 simpr1 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> A e. V )
6 simpr3 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> C e. V )
7 1 sps3wwlks2on 
 |-  ( ( G e. USPGraph /\ A e. V /\ C e. V ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
8 4 5 6 7 syl3anc 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
9 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
10 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
11 1 10 upgr2wlk 
 |-  ( G e. UPGraph -> ( ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) <-> ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { ( <" A B C "> ` 0 ) , ( <" A B C "> ` 1 ) } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { ( <" A B C "> ` 1 ) , ( <" A B C "> ` 2 ) } ) ) ) )
12 9 11 syl 
 |-  ( G e. USGraph -> ( ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) <-> ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { ( <" A B C "> ` 0 ) , ( <" A B C "> ` 1 ) } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { ( <" A B C "> ` 1 ) , ( <" A B C "> ` 2 ) } ) ) ) )
13 12 adantr 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) <-> ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { ( <" A B C "> ` 0 ) , ( <" A B C "> ` 1 ) } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { ( <" A B C "> ` 1 ) , ( <" A B C "> ` 2 ) } ) ) ) )
14 s3fv0 
 |-  ( A e. V -> ( <" A B C "> ` 0 ) = A )
15 14 3ad2ant1 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( <" A B C "> ` 0 ) = A )
16 s3fv1 
 |-  ( B e. V -> ( <" A B C "> ` 1 ) = B )
17 16 3ad2ant2 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( <" A B C "> ` 1 ) = B )
18 15 17 preq12d 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> { ( <" A B C "> ` 0 ) , ( <" A B C "> ` 1 ) } = { A , B } )
19 18 eqeq2d 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { ( <" A B C "> ` 0 ) , ( <" A B C "> ` 1 ) } <-> ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } ) )
20 s3fv2 
 |-  ( C e. V -> ( <" A B C "> ` 2 ) = C )
21 20 3ad2ant3 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( <" A B C "> ` 2 ) = C )
22 17 21 preq12d 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> { ( <" A B C "> ` 1 ) , ( <" A B C "> ` 2 ) } = { B , C } )
23 22 eqeq2d 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( ( iEdg ` G ) ` ( f ` 1 ) ) = { ( <" A B C "> ` 1 ) , ( <" A B C "> ` 2 ) } <-> ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) )
24 19 23 anbi12d 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { ( <" A B C "> ` 0 ) , ( <" A B C "> ` 1 ) } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { ( <" A B C "> ` 1 ) , ( <" A B C "> ` 2 ) } ) <-> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) )
25 24 adantl 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { ( <" A B C "> ` 0 ) , ( <" A B C "> ` 1 ) } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { ( <" A B C "> ` 1 ) , ( <" A B C "> ` 2 ) } ) <-> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) )
26 25 3anbi3d 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { ( <" A B C "> ` 0 ) , ( <" A B C "> ` 1 ) } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { ( <" A B C "> ` 1 ) , ( <" A B C "> ` 2 ) } ) ) <-> ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) ) )
27 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
28 10 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
29 fdmrn 
 |-  ( Fun ( iEdg ` G ) <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) )
30 simpr 
 |-  ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) )
31 id 
 |-  ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) -> f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) )
32 c0ex 
 |-  0 e. _V
33 32 prid1 
 |-  0 e. { 0 , 1 }
34 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
35 33 34 eleqtrri 
 |-  0 e. ( 0 ..^ 2 )
36 35 a1i 
 |-  ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) -> 0 e. ( 0 ..^ 2 ) )
37 31 36 ffvelcdmd 
 |-  ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) -> ( f ` 0 ) e. dom ( iEdg ` G ) )
38 37 adantr 
 |-  ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) ) -> ( f ` 0 ) e. dom ( iEdg ` G ) )
39 30 38 ffvelcdmd 
 |-  ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) )
40 1ex 
 |-  1 e. _V
41 40 prid2 
 |-  1 e. { 0 , 1 }
42 41 34 eleqtrri 
 |-  1 e. ( 0 ..^ 2 )
43 42 a1i 
 |-  ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) -> 1 e. ( 0 ..^ 2 ) )
44 31 43 ffvelcdmd 
 |-  ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) -> ( f ` 1 ) e. dom ( iEdg ` G ) )
45 44 adantr 
 |-  ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) ) -> ( f ` 1 ) e. dom ( iEdg ` G ) )
46 30 45 ffvelcdmd 
 |-  ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) )
47 39 46 jca 
 |-  ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) ) -> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) ) )
48 47 ex 
 |-  ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) -> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) ) ) )
49 48 3ad2ant1 
 |-  ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) -> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) ) ) )
50 49 com12 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ran ( iEdg ` G ) -> ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) -> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) ) ) )
51 29 50 sylbi 
 |-  ( Fun ( iEdg ` G ) -> ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) -> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) ) ) )
52 27 28 51 3syl 
 |-  ( G e. USGraph -> ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) -> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) ) ) )
53 52 imp 
 |-  ( ( G e. USGraph /\ ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) ) -> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) ) )
54 eqcom 
 |-  ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } <-> { A , B } = ( ( iEdg ` G ) ` ( f ` 0 ) ) )
55 54 biimpi 
 |-  ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } -> { A , B } = ( ( iEdg ` G ) ` ( f ` 0 ) ) )
56 55 adantr 
 |-  ( ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) -> { A , B } = ( ( iEdg ` G ) ` ( f ` 0 ) ) )
57 56 3ad2ant3 
 |-  ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) -> { A , B } = ( ( iEdg ` G ) ` ( f ` 0 ) ) )
58 57 adantl 
 |-  ( ( G e. USGraph /\ ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) ) -> { A , B } = ( ( iEdg ` G ) ` ( f ` 0 ) ) )
59 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
60 2 59 eqtri 
 |-  E = ran ( iEdg ` G )
61 60 a1i 
 |-  ( ( G e. USGraph /\ ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) ) -> E = ran ( iEdg ` G ) )
62 58 61 eleq12d 
 |-  ( ( G e. USGraph /\ ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) ) -> ( { A , B } e. E <-> ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) ) )
63 eqcom 
 |-  ( ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } <-> { B , C } = ( ( iEdg ` G ) ` ( f ` 1 ) ) )
64 63 biimpi 
 |-  ( ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } -> { B , C } = ( ( iEdg ` G ) ` ( f ` 1 ) ) )
65 64 adantl 
 |-  ( ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) -> { B , C } = ( ( iEdg ` G ) ` ( f ` 1 ) ) )
66 65 3ad2ant3 
 |-  ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) -> { B , C } = ( ( iEdg ` G ) ` ( f ` 1 ) ) )
67 66 adantl 
 |-  ( ( G e. USGraph /\ ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) ) -> { B , C } = ( ( iEdg ` G ) ` ( f ` 1 ) ) )
68 67 61 eleq12d 
 |-  ( ( G e. USGraph /\ ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) ) -> ( { B , C } e. E <-> ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) ) )
69 62 68 anbi12d 
 |-  ( ( G e. USGraph /\ ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) ) -> ( ( { A , B } e. E /\ { B , C } e. E ) <-> ( ( ( iEdg ` G ) ` ( f ` 0 ) ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) e. ran ( iEdg ` G ) ) ) )
70 53 69 mpbird 
 |-  ( ( G e. USGraph /\ ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) ) -> ( { A , B } e. E /\ { B , C } e. E ) )
71 70 ex 
 |-  ( G e. USGraph -> ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) -> ( { A , B } e. E /\ { B , C } e. E ) ) )
72 71 adantr 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { A , B } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { B , C } ) ) -> ( { A , B } e. E /\ { B , C } e. E ) ) )
73 26 72 sylbid 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( f : ( 0 ..^ 2 ) --> dom ( iEdg ` G ) /\ <" A B C "> : ( 0 ... 2 ) --> V /\ ( ( ( iEdg ` G ) ` ( f ` 0 ) ) = { ( <" A B C "> ` 0 ) , ( <" A B C "> ` 1 ) } /\ ( ( iEdg ` G ) ` ( f ` 1 ) ) = { ( <" A B C "> ` 1 ) , ( <" A B C "> ` 2 ) } ) ) -> ( { A , B } e. E /\ { B , C } e. E ) ) )
74 13 73 sylbid 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) -> ( { A , B } e. E /\ { B , C } e. E ) ) )
75 74 exlimdv 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) -> ( { A , B } e. E /\ { B , C } e. E ) ) )
76 usgrumgr 
 |-  ( G e. USGraph -> G e. UMGraph )
77 76 3ad2ant1 
 |-  ( ( G e. USGraph /\ { A , B } e. E /\ { B , C } e. E ) -> G e. UMGraph )
78 simp2 
 |-  ( ( G e. USGraph /\ { A , B } e. E /\ { B , C } e. E ) -> { A , B } e. E )
79 simp3 
 |-  ( ( G e. USGraph /\ { A , B } e. E /\ { B , C } e. E ) -> { B , C } e. E )
80 2 umgr2wlk 
 |-  ( ( G e. UMGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) )
81 77 78 79 80 syl3anc 
 |-  ( ( G e. USGraph /\ { A , B } e. E /\ { B , C } e. E ) -> E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) )
82 wlklenvp1 
 |-  ( f ( Walks ` G ) p -> ( # ` p ) = ( ( # ` f ) + 1 ) )
83 oveq1 
 |-  ( ( # ` f ) = 2 -> ( ( # ` f ) + 1 ) = ( 2 + 1 ) )
84 2p1e3 
 |-  ( 2 + 1 ) = 3
85 83 84 eqtrdi 
 |-  ( ( # ` f ) = 2 -> ( ( # ` f ) + 1 ) = 3 )
86 85 adantr 
 |-  ( ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( ( # ` f ) + 1 ) = 3 )
87 82 86 sylan9eq 
 |-  ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( # ` p ) = 3 )
88 eqcom 
 |-  ( A = ( p ` 0 ) <-> ( p ` 0 ) = A )
89 eqcom 
 |-  ( B = ( p ` 1 ) <-> ( p ` 1 ) = B )
90 eqcom 
 |-  ( C = ( p ` 2 ) <-> ( p ` 2 ) = C )
91 88 89 90 3anbi123i 
 |-  ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) <-> ( ( p ` 0 ) = A /\ ( p ` 1 ) = B /\ ( p ` 2 ) = C ) )
92 91 biimpi 
 |-  ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( ( p ` 0 ) = A /\ ( p ` 1 ) = B /\ ( p ` 2 ) = C ) )
93 92 adantl 
 |-  ( ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( ( p ` 0 ) = A /\ ( p ` 1 ) = B /\ ( p ` 2 ) = C ) )
94 93 adantl 
 |-  ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( ( p ` 0 ) = A /\ ( p ` 1 ) = B /\ ( p ` 2 ) = C ) )
95 87 94 jca 
 |-  ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( ( # ` p ) = 3 /\ ( ( p ` 0 ) = A /\ ( p ` 1 ) = B /\ ( p ` 2 ) = C ) ) )
96 1 wlkpwrd 
 |-  ( f ( Walks ` G ) p -> p e. Word V )
97 85 eqeq2d 
 |-  ( ( # ` f ) = 2 -> ( ( # ` p ) = ( ( # ` f ) + 1 ) <-> ( # ` p ) = 3 ) )
98 97 adantl 
 |-  ( ( p e. Word V /\ ( # ` f ) = 2 ) -> ( ( # ` p ) = ( ( # ` f ) + 1 ) <-> ( # ` p ) = 3 ) )
99 simp1 
 |-  ( ( p e. Word V /\ ( # ` p ) = 3 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> p e. Word V )
100 oveq2 
 |-  ( ( # ` p ) = 3 -> ( 0 ..^ ( # ` p ) ) = ( 0 ..^ 3 ) )
101 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
102 100 101 eqtrdi 
 |-  ( ( # ` p ) = 3 -> ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } )
103 32 tpid1 
 |-  0 e. { 0 , 1 , 2 }
104 eleq2 
 |-  ( ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } -> ( 0 e. ( 0 ..^ ( # ` p ) ) <-> 0 e. { 0 , 1 , 2 } ) )
105 103 104 mpbiri 
 |-  ( ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } -> 0 e. ( 0 ..^ ( # ` p ) ) )
106 wrdsymbcl 
 |-  ( ( p e. Word V /\ 0 e. ( 0 ..^ ( # ` p ) ) ) -> ( p ` 0 ) e. V )
107 105 106 sylan2 
 |-  ( ( p e. Word V /\ ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } ) -> ( p ` 0 ) e. V )
108 40 tpid2 
 |-  1 e. { 0 , 1 , 2 }
109 eleq2 
 |-  ( ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } -> ( 1 e. ( 0 ..^ ( # ` p ) ) <-> 1 e. { 0 , 1 , 2 } ) )
110 108 109 mpbiri 
 |-  ( ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } -> 1 e. ( 0 ..^ ( # ` p ) ) )
111 wrdsymbcl 
 |-  ( ( p e. Word V /\ 1 e. ( 0 ..^ ( # ` p ) ) ) -> ( p ` 1 ) e. V )
112 110 111 sylan2 
 |-  ( ( p e. Word V /\ ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } ) -> ( p ` 1 ) e. V )
113 2ex 
 |-  2 e. _V
114 113 tpid3 
 |-  2 e. { 0 , 1 , 2 }
115 eleq2 
 |-  ( ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } -> ( 2 e. ( 0 ..^ ( # ` p ) ) <-> 2 e. { 0 , 1 , 2 } ) )
116 114 115 mpbiri 
 |-  ( ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } -> 2 e. ( 0 ..^ ( # ` p ) ) )
117 wrdsymbcl 
 |-  ( ( p e. Word V /\ 2 e. ( 0 ..^ ( # ` p ) ) ) -> ( p ` 2 ) e. V )
118 116 117 sylan2 
 |-  ( ( p e. Word V /\ ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } ) -> ( p ` 2 ) e. V )
119 107 112 118 3jca 
 |-  ( ( p e. Word V /\ ( 0 ..^ ( # ` p ) ) = { 0 , 1 , 2 } ) -> ( ( p ` 0 ) e. V /\ ( p ` 1 ) e. V /\ ( p ` 2 ) e. V ) )
120 102 119 sylan2 
 |-  ( ( p e. Word V /\ ( # ` p ) = 3 ) -> ( ( p ` 0 ) e. V /\ ( p ` 1 ) e. V /\ ( p ` 2 ) e. V ) )
121 120 3adant3 
 |-  ( ( p e. Word V /\ ( # ` p ) = 3 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( ( p ` 0 ) e. V /\ ( p ` 1 ) e. V /\ ( p ` 2 ) e. V ) )
122 eleq1 
 |-  ( A = ( p ` 0 ) -> ( A e. V <-> ( p ` 0 ) e. V ) )
123 122 3ad2ant1 
 |-  ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( A e. V <-> ( p ` 0 ) e. V ) )
124 eleq1 
 |-  ( B = ( p ` 1 ) -> ( B e. V <-> ( p ` 1 ) e. V ) )
125 124 3ad2ant2 
 |-  ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( B e. V <-> ( p ` 1 ) e. V ) )
126 eleq1 
 |-  ( C = ( p ` 2 ) -> ( C e. V <-> ( p ` 2 ) e. V ) )
127 126 3ad2ant3 
 |-  ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( C e. V <-> ( p ` 2 ) e. V ) )
128 123 125 127 3anbi123d 
 |-  ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( ( A e. V /\ B e. V /\ C e. V ) <-> ( ( p ` 0 ) e. V /\ ( p ` 1 ) e. V /\ ( p ` 2 ) e. V ) ) )
129 128 3ad2ant3 
 |-  ( ( p e. Word V /\ ( # ` p ) = 3 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( ( A e. V /\ B e. V /\ C e. V ) <-> ( ( p ` 0 ) e. V /\ ( p ` 1 ) e. V /\ ( p ` 2 ) e. V ) ) )
130 121 129 mpbird 
 |-  ( ( p e. Word V /\ ( # ` p ) = 3 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( A e. V /\ B e. V /\ C e. V ) )
131 99 130 jca 
 |-  ( ( p e. Word V /\ ( # ` p ) = 3 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( p e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) )
132 131 3exp 
 |-  ( p e. Word V -> ( ( # ` p ) = 3 -> ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( p e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) ) ) )
133 132 adantr 
 |-  ( ( p e. Word V /\ ( # ` f ) = 2 ) -> ( ( # ` p ) = 3 -> ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( p e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) ) ) )
134 98 133 sylbid 
 |-  ( ( p e. Word V /\ ( # ` f ) = 2 ) -> ( ( # ` p ) = ( ( # ` f ) + 1 ) -> ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( p e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) ) ) )
135 134 impancom 
 |-  ( ( p e. Word V /\ ( # ` p ) = ( ( # ` f ) + 1 ) ) -> ( ( # ` f ) = 2 -> ( ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) -> ( p e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) ) ) )
136 135 impd 
 |-  ( ( p e. Word V /\ ( # ` p ) = ( ( # ` f ) + 1 ) ) -> ( ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( p e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) ) )
137 96 82 136 syl2anc 
 |-  ( f ( Walks ` G ) p -> ( ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( p e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) ) )
138 137 imp 
 |-  ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( p e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) )
139 eqwrds3 
 |-  ( ( p e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( p = <" A B C "> <-> ( ( # ` p ) = 3 /\ ( ( p ` 0 ) = A /\ ( p ` 1 ) = B /\ ( p ` 2 ) = C ) ) ) )
140 138 139 syl 
 |-  ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( p = <" A B C "> <-> ( ( # ` p ) = 3 /\ ( ( p ` 0 ) = A /\ ( p ` 1 ) = B /\ ( p ` 2 ) = C ) ) ) )
141 95 140 mpbird 
 |-  ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> p = <" A B C "> )
142 141 breq2d 
 |-  ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( f ( Walks ` G ) p <-> f ( Walks ` G ) <" A B C "> ) )
143 142 biimpd 
 |-  ( ( f ( Walks ` G ) p /\ ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( f ( Walks ` G ) p -> f ( Walks ` G ) <" A B C "> ) )
144 143 ex 
 |-  ( f ( Walks ` G ) p -> ( ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( f ( Walks ` G ) p -> f ( Walks ` G ) <" A B C "> ) ) )
145 144 pm2.43a 
 |-  ( f ( Walks ` G ) p -> ( ( ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> f ( Walks ` G ) <" A B C "> ) )
146 145 3impib 
 |-  ( ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> f ( Walks ` G ) <" A B C "> )
147 146 adantl 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> f ( Walks ` G ) <" A B C "> )
148 simpr2 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( # ` f ) = 2 )
149 147 148 jca 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) -> ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) )
150 149 ex 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
151 150 exlimdv 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
152 151 eximdv 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( E. f E. p ( f ( Walks ` G ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) -> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
153 81 152 syl5com 
 |-  ( ( G e. USGraph /\ { A , B } e. E /\ { B , C } e. E ) -> ( ( A e. V /\ B e. V /\ C e. V ) -> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
154 153 3expib 
 |-  ( G e. USGraph -> ( ( { A , B } e. E /\ { B , C } e. E ) -> ( ( A e. V /\ B e. V /\ C e. V ) -> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) ) )
155 154 com23 
 |-  ( G e. USGraph -> ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( { A , B } e. E /\ { B , C } e. E ) -> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) ) )
156 155 imp 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( { A , B } e. E /\ { B , C } e. E ) -> E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) ) )
157 75 156 impbid 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( E. f ( f ( Walks ` G ) <" A B C "> /\ ( # ` f ) = 2 ) <-> ( { A , B } e. E /\ { B , C } e. E ) ) )
158 8 157 bitrd 
 |-  ( ( G e. USGraph /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> ( { A , B } e. E /\ { B , C } e. E ) ) )