Metamath Proof Explorer

Theorem usgr2trlncl

Description: In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021) (Proof shortened by AV, 31-Oct-2021)

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

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 upgrf1istrl 
 |-  ( G e. UPGraph -> ( F ( Trails ` G ) P <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
5 1 4 syl 
 |-  ( G e. USGraph -> ( F ( Trails ` G ) P <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
6 eqidd 
 |-  ( ( # ` F ) = 2 -> F = F )
7 oveq2 
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) )
8 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
9 7 8 eqtrdi 
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = { 0 , 1 } )
10 eqidd 
 |-  ( ( # ` F ) = 2 -> dom ( iEdg ` G ) = dom ( iEdg ` G ) )
11 6 9 10 f1eq123d 
 |-  ( ( # ` F ) = 2 -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) <-> F : { 0 , 1 } -1-1-> dom ( iEdg ` G ) ) )
12 9 raleqdv 
 |-  ( ( # ` F ) = 2 -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> A. i e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
13 2wlklem 
 |-  ( A. i e. { 0 , 1 } ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
14 12 13 bitrdi 
 |-  ( ( # ` F ) = 2 -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) )
15 11 14 anbi12d 
 |-  ( ( # ` F ) = 2 -> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) <-> ( F : { 0 , 1 } -1-1-> dom ( iEdg ` G ) /\ ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
16 15 adantl 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) <-> ( F : { 0 , 1 } -1-1-> dom ( iEdg ` G ) /\ ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
17 c0ex 
 |-  0 e. _V
18 1ex 
 |-  1 e. _V
19 17 18 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
20 0ne1 
 |-  0 =/= 1
21 eqid 
 |-  { 0 , 1 } = { 0 , 1 }
22 21 f12dfv 
 |-  ( ( ( 0 e. _V /\ 1 e. _V ) /\ 0 =/= 1 ) -> ( F : { 0 , 1 } -1-1-> dom ( iEdg ` G ) <-> ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) ) )
23 19 20 22 mp2an 
 |-  ( F : { 0 , 1 } -1-1-> dom ( iEdg ` G ) <-> ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) )
24 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
25 3 24 usgrf1oedg 
 |-  ( G e. USGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) )
26 f1of1 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) )
27 id 
 |-  ( F : { 0 , 1 } --> dom ( iEdg ` G ) -> F : { 0 , 1 } --> dom ( iEdg ` G ) )
28 17 prid1 
 |-  0 e. { 0 , 1 }
29 28 a1i 
 |-  ( F : { 0 , 1 } --> dom ( iEdg ` G ) -> 0 e. { 0 , 1 } )
30 27 29 ffvelrnd 
 |-  ( F : { 0 , 1 } --> dom ( iEdg ` G ) -> ( F ` 0 ) e. dom ( iEdg ` G ) )
31 18 prid2 
 |-  1 e. { 0 , 1 }
32 31 a1i 
 |-  ( F : { 0 , 1 } --> dom ( iEdg ` G ) -> 1 e. { 0 , 1 } )
33 27 32 ffvelrnd 
 |-  ( F : { 0 , 1 } --> dom ( iEdg ` G ) -> ( F ` 1 ) e. dom ( iEdg ` G ) )
34 30 33 jca 
 |-  ( F : { 0 , 1 } --> dom ( iEdg ` G ) -> ( ( F ` 0 ) e. dom ( iEdg ` G ) /\ ( F ` 1 ) e. dom ( iEdg ` G ) ) )
35 34 anim1ci 
 |-  ( ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) /\ ( ( F ` 0 ) e. dom ( iEdg ` G ) /\ ( F ` 1 ) e. dom ( iEdg ` G ) ) ) )
36 f1veqaeq 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) /\ ( ( F ` 0 ) e. dom ( iEdg ` G ) /\ ( F ` 1 ) e. dom ( iEdg ` G ) ) ) -> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = ( ( iEdg ` G ) ` ( F ` 1 ) ) -> ( F ` 0 ) = ( F ` 1 ) ) )
37 35 36 syl 
 |-  ( ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) ) -> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = ( ( iEdg ` G ) ` ( F ` 1 ) ) -> ( F ` 0 ) = ( F ` 1 ) ) )
38 37 necon3d 
 |-  ( ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) ) -> ( ( F ` 0 ) =/= ( F ` 1 ) -> ( ( iEdg ` G ) ` ( F ` 0 ) ) =/= ( ( iEdg ` G ) ` ( F ` 1 ) ) ) )
39 simpl 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } )
40 simpr 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } )
41 39 40 neeq12d 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) =/= ( ( iEdg ` G ) ` ( F ` 1 ) ) <-> { ( P ` 0 ) , ( P ` 1 ) } =/= { ( P ` 1 ) , ( P ` 2 ) } ) )
42 preq1 
 |-  ( ( P ` 0 ) = ( P ` 2 ) -> { ( P ` 0 ) , ( P ` 1 ) } = { ( P ` 2 ) , ( P ` 1 ) } )
43 prcom 
 |-  { ( P ` 2 ) , ( P ` 1 ) } = { ( P ` 1 ) , ( P ` 2 ) }
44 42 43 eqtrdi 
 |-  ( ( P ` 0 ) = ( P ` 2 ) -> { ( P ` 0 ) , ( P ` 1 ) } = { ( P ` 1 ) , ( P ` 2 ) } )
45 44 necon3i 
 |-  ( { ( P ` 0 ) , ( P ` 1 ) } =/= { ( P ` 1 ) , ( P ` 2 ) } -> ( P ` 0 ) =/= ( P ` 2 ) )
46 41 45 syl6bi 
 |-  ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( ( ( iEdg ` G ) ` ( F ` 0 ) ) =/= ( ( iEdg ` G ) ` ( F ` 1 ) ) -> ( P ` 0 ) =/= ( P ` 2 ) ) )
47 46 com12 
 |-  ( ( ( iEdg ` G ) ` ( F ` 0 ) ) =/= ( ( iEdg ` G ) ` ( F ` 1 ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) )
48 47 a1d 
 |-  ( ( ( iEdg ` G ) ` ( F ` 0 ) ) =/= ( ( iEdg ` G ) ` ( F ` 1 ) ) -> ( G e. USGraph -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) ) )
49 38 48 syl6 
 |-  ( ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) ) -> ( ( F ` 0 ) =/= ( F ` 1 ) -> ( G e. USGraph -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) ) ) )
50 49 expcom 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) -> ( F : { 0 , 1 } --> dom ( iEdg ` G ) -> ( ( F ` 0 ) =/= ( F ` 1 ) -> ( G e. USGraph -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) ) ) ) )
51 50 impd 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) -> ( ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( G e. USGraph -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) ) ) )
52 51 com23 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( Edg ` G ) -> ( G e. USGraph -> ( ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) ) ) )
53 26 52 syl 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ( Edg ` G ) -> ( G e. USGraph -> ( ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) ) ) )
54 25 53 mpcom 
 |-  ( G e. USGraph -> ( ( F : { 0 , 1 } --> dom ( iEdg ` G ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) ) )
55 23 54 syl5bi 
 |-  ( G e. USGraph -> ( F : { 0 , 1 } -1-1-> dom ( iEdg ` G ) -> ( ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) ) )
56 55 impd 
 |-  ( G e. USGraph -> ( ( F : { 0 , 1 } -1-1-> dom ( iEdg ` G ) /\ ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) -> ( P ` 0 ) =/= ( P ` 2 ) ) )
57 56 adantr 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( F : { 0 , 1 } -1-1-> dom ( iEdg ` G ) /\ ( ( ( iEdg ` G ) ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( ( iEdg ` G ) ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) -> ( P ` 0 ) =/= ( P ` 2 ) ) )
58 16 57 sylbid 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) )
59 58 com12 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( P ` 0 ) =/= ( P ` 2 ) ) )
60 59 3adant2 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( P ` 0 ) =/= ( P ` 2 ) ) )
61 60 expdcom 
 |-  ( G e. USGraph -> ( ( # ` F ) = 2 -> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( P ` 0 ) =/= ( P ` 2 ) ) ) )
62 61 com23 
 |-  ( G e. USGraph -> ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( ( # ` F ) = 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) )
63 5 62 sylbid 
 |-  ( G e. USGraph -> ( F ( Trails ` G ) P -> ( ( # ` F ) = 2 -> ( P ` 0 ) =/= ( P ` 2 ) ) ) )
64 63 com23 
 |-  ( G e. USGraph -> ( ( # ` F ) = 2 -> ( F ( Trails ` G ) P -> ( P ` 0 ) =/= ( P ` 2 ) ) ) )
65 64 imp 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P -> ( P ` 0 ) =/= ( P ` 2 ) ) )