Metamath Proof Explorer

Theorem usgr2wlkneq

Description: The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 26-Jan-2021)

Ref Expression
Assertion usgr2wlkneq 
|- ( ( ( G e. USGraph /\ F ( Walks ` G ) P ) /\ ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) )

Proof

Step Hyp Ref Expression
1 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
4 2 3 upgriswlk 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
5 1 4 syl 
 |-  ( G e. USGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
6 2wlklem 
 |-  ( A. k e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
7 simplll 
 |-  ( ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) /\ P : ( 0 ... 2 ) --> ( Vtx ` G ) ) -> G e. USGraph )
8 fvex 
 |-  ( P ` 0 ) e. _V
9 3 usgrnloopv 
 |-  ( ( G e. USGraph /\ ( P ` 0 ) e. _V ) -> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } -> ( P ` 0 ) =/= ( P ` 1 ) ) )
10 7 8 9 sylancl 
 |-  ( ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) /\ P : ( 0 ... 2 ) --> ( Vtx ` G ) ) -> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } -> ( P ` 0 ) =/= ( P ` 1 ) ) )
11 fvex 
 |-  ( P ` 1 ) e. _V
12 3 usgrnloopv 
 |-  ( ( G e. USGraph /\ ( P ` 1 ) e. _V ) -> ( ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } -> ( P ` 1 ) =/= ( P ` 2 ) ) )
13 7 11 12 sylancl 
 |-  ( ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) /\ P : ( 0 ... 2 ) --> ( Vtx ` G ) ) -> ( ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } -> ( P ` 1 ) =/= ( P ` 2 ) ) )
14 10 13 anim12d 
 |-  ( ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) /\ P : ( 0 ... 2 ) --> ( Vtx ` G ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) ) )
15 fveqeq2 
 |-  ( ( F ` 0 ) = ( F ` 1 ) -> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } <-> ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 0 ) , ( P ` 1 ) } ) )
16 eqtr2 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> { ( P ` 0 ) , ( P ` 1 ) } = { ( P ` 1 ) , ( P ` 2 ) } )
17 prcom 
 |-  { ( P ` 1 ) , ( P ` 2 ) } = { ( P ` 2 ) , ( P ` 1 ) }
18 17 eqeq2i 
 |-  ( { ( P ` 0 ) , ( P ` 1 ) } = { ( P ` 1 ) , ( P ` 2 ) } <-> { ( P ` 0 ) , ( P ` 1 ) } = { ( P ` 2 ) , ( P ` 1 ) } )
19 fvex 
 |-  ( P ` 2 ) e. _V
20 8 19 preqr1 
 |-  ( { ( P ` 0 ) , ( P ` 1 ) } = { ( P ` 2 ) , ( P ` 1 ) } -> ( P ` 0 ) = ( P ` 2 ) )
21 18 20 sylbi 
 |-  ( { ( P ` 0 ) , ( P ` 1 ) } = { ( P ` 1 ) , ( P ` 2 ) } -> ( P ` 0 ) = ( P ` 2 ) )
22 16 21 syl 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) = ( P ` 2 ) )
23 22 ex 
 |-  ( ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 0 ) , ( P ` 1 ) } -> ( ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } -> ( P ` 0 ) = ( P ` 2 ) ) )
24 15 23 biimtrdi 
 |-  ( ( F ` 0 ) = ( F ` 1 ) -> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } -> ( ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } -> ( P ` 0 ) = ( P ` 2 ) ) ) )
25 24 impd 
 |-  ( ( F ` 0 ) = ( F ` 1 ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) = ( P ` 2 ) ) )
26 25 com12 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( F ` 0 ) = ( F ` 1 ) -> ( P ` 0 ) = ( P ` 2 ) ) )
27 26 necon3d 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> ( F ` 0 ) =/= ( F ` 1 ) ) )
28 27 com12 
 |-  ( ( P ` 0 ) =/= ( P ` 2 ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( F ` 0 ) =/= ( F ` 1 ) ) )
29 28 adantr 
 |-  ( ( ( P ` 0 ) =/= ( P ` 2 ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( F ` 0 ) =/= ( F ` 1 ) ) )
30 simpl 
 |-  ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) -> ( P ` 0 ) =/= ( P ` 1 ) )
31 30 adantl 
 |-  ( ( ( P ` 0 ) =/= ( P ` 2 ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) ) -> ( P ` 0 ) =/= ( P ` 1 ) )
32 simpl 
 |-  ( ( ( P ` 0 ) =/= ( P ` 2 ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) ) -> ( P ` 0 ) =/= ( P ` 2 ) )
33 simprr 
 |-  ( ( ( P ` 0 ) =/= ( P ` 2 ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) ) -> ( P ` 1 ) =/= ( P ` 2 ) )
34 31 32 33 3jca 
 |-  ( ( ( P ` 0 ) =/= ( P ` 2 ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) ) -> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) )
35 29 34 jctild 
 |-  ( ( ( P ` 0 ) =/= ( P ` 2 ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) )
36 35 ex 
 |-  ( ( P ` 0 ) =/= ( P ` 2 ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) )
37 36 com23 
 |-  ( ( P ` 0 ) =/= ( P ` 2 ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) )
38 37 adantl 
 |-  ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) )
39 38 adantr 
 |-  ( ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) /\ P : ( 0 ... 2 ) --> ( Vtx ` G ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) )
40 14 39 mpdd 
 |-  ( ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) /\ P : ( 0 ... 2 ) --> ( Vtx ` G ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) )
41 6 40 biimtrid 
 |-  ( ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) /\ P : ( 0 ... 2 ) --> ( Vtx ` G ) ) -> ( A. k e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) )
42 41 ex 
 |-  ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( P : ( 0 ... 2 ) --> ( Vtx ` G ) -> ( A. k e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) )
43 42 com23 
 |-  ( ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( A. k e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( P : ( 0 ... 2 ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) )
44 43 ex 
 |-  ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> ( A. k e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( P : ( 0 ... 2 ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) ) )
45 fveq2 
 |-  ( ( # ` F ) = 2 -> ( P ` ( # ` F ) ) = ( P ` 2 ) )
46 45 neeq2d 
 |-  ( ( # ` F ) = 2 -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> ( P ` 0 ) =/= ( P ` 2 ) ) )
47 oveq2 
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) )
48 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
49 47 48 eqtrdi 
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = { 0 , 1 } )
50 49 raleqdv 
 |-  ( ( # ` F ) = 2 -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> A. k e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
51 oveq2 
 |-  ( ( # ` F ) = 2 -> ( 0 ... ( # ` F ) ) = ( 0 ... 2 ) )
52 51 feq2d 
 |-  ( ( # ` F ) = 2 -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) <-> P : ( 0 ... 2 ) --> ( Vtx ` G ) ) )
53 52 imbi1d 
 |-  ( ( # ` F ) = 2 -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) <-> ( P : ( 0 ... 2 ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) )
54 50 53 imbi12d 
 |-  ( ( # ` F ) = 2 -> ( ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) <-> ( A. k e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( P : ( 0 ... 2 ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) ) )
55 46 54 imbi12d 
 |-  ( ( # ` F ) = 2 -> ( ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) ) <-> ( ( P ` 0 ) =/= ( P ` 2 ) -> ( A. k e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( P : ( 0 ... 2 ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) ) ) )
56 44 55 syl5ibrcom 
 |-  ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) -> ( ( # ` F ) = 2 -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) ) ) )
57 56 impd 
 |-  ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) -> ( ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) ) )
58 57 com24 
 |-  ( ( G e. USGraph /\ F e. Word dom ( iEdg ` G ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) ) )
59 58 ex 
 |-  ( G e. USGraph -> ( F e. Word dom ( iEdg ` G ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> ( ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) ) ) )
60 59 3impd 
 |-  ( G e. USGraph -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) )
61 5 60 sylbid 
 |-  ( G e. USGraph -> ( F ( Walks ` G ) P -> ( ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) ) )
62 61 imp31 
 |-  ( ( ( G e. USGraph /\ F ( Walks ` G ) P ) /\ ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) )