Metamath Proof Explorer

Theorem cycl3grtrilem

Description: Lemma for cycl3grtri . (Contributed by AV, 5-Oct-2025)

Ref Expression
Assertion cycl3grtrilem 
|- ( ( ( G e. UPGraph /\ F ( Paths ` G ) P ) /\ ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) )

Proof

Step Hyp Ref Expression
1 pthiswlk 
 |-  ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 2 upgrwlkvtxedg 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> A. x e. ( 0 ..^ ( # ` F ) ) { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) )
4 1 3 sylan2 
 |-  ( ( G e. UPGraph /\ F ( Paths ` G ) P ) -> A. x e. ( 0 ..^ ( # ` F ) ) { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) )
5 4 adantr 
 |-  ( ( ( G e. UPGraph /\ F ( Paths ` G ) P ) /\ ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) ) -> A. x e. ( 0 ..^ ( # ` F ) ) { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) )
6 oveq2 
 |-  ( ( # ` F ) = 3 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 3 ) )
7 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
8 6 7 eqtrdi 
 |-  ( ( # ` F ) = 3 -> ( 0 ..^ ( # ` F ) ) = { 0 , 1 , 2 } )
9 8 adantl 
 |-  ( ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) -> ( 0 ..^ ( # ` F ) ) = { 0 , 1 , 2 } )
10 9 adantl 
 |-  ( ( ( G e. UPGraph /\ F ( Paths ` G ) P ) /\ ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) ) -> ( 0 ..^ ( # ` F ) ) = { 0 , 1 , 2 } )
11 10 raleqdv 
 |-  ( ( ( G e. UPGraph /\ F ( Paths ` G ) P ) /\ ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) <-> A. x e. { 0 , 1 , 2 } { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) ) )
12 fveq2 
 |-  ( ( # ` F ) = 3 -> ( P ` ( # ` F ) ) = ( P ` 3 ) )
13 12 eqeq2d 
 |-  ( ( # ` F ) = 3 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( P ` 0 ) = ( P ` 3 ) ) )
14 c0ex 
 |-  0 e. _V
15 1ex 
 |-  1 e. _V
16 2ex 
 |-  2 e. _V
17 fveq2 
 |-  ( x = 0 -> ( P ` x ) = ( P ` 0 ) )
18 fv0p1e1 
 |-  ( x = 0 -> ( P ` ( x + 1 ) ) = ( P ` 1 ) )
19 17 18 preq12d 
 |-  ( x = 0 -> { ( P ` x ) , ( P ` ( x + 1 ) ) } = { ( P ` 0 ) , ( P ` 1 ) } )
20 19 eleq1d 
 |-  ( x = 0 -> ( { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) <-> { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) ) )
21 fveq2 
 |-  ( x = 1 -> ( P ` x ) = ( P ` 1 ) )
22 oveq1 
 |-  ( x = 1 -> ( x + 1 ) = ( 1 + 1 ) )
23 1p1e2 
 |-  ( 1 + 1 ) = 2
24 22 23 eqtrdi 
 |-  ( x = 1 -> ( x + 1 ) = 2 )
25 24 fveq2d 
 |-  ( x = 1 -> ( P ` ( x + 1 ) ) = ( P ` 2 ) )
26 21 25 preq12d 
 |-  ( x = 1 -> { ( P ` x ) , ( P ` ( x + 1 ) ) } = { ( P ` 1 ) , ( P ` 2 ) } )
27 26 eleq1d 
 |-  ( x = 1 -> ( { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) <-> { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) )
28 fveq2 
 |-  ( x = 2 -> ( P ` x ) = ( P ` 2 ) )
29 oveq1 
 |-  ( x = 2 -> ( x + 1 ) = ( 2 + 1 ) )
30 2p1e3 
 |-  ( 2 + 1 ) = 3
31 29 30 eqtrdi 
 |-  ( x = 2 -> ( x + 1 ) = 3 )
32 31 fveq2d 
 |-  ( x = 2 -> ( P ` ( x + 1 ) ) = ( P ` 3 ) )
33 28 32 preq12d 
 |-  ( x = 2 -> { ( P ` x ) , ( P ` ( x + 1 ) ) } = { ( P ` 2 ) , ( P ` 3 ) } )
34 33 eleq1d 
 |-  ( x = 2 -> ( { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) <-> { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) ) )
35 14 15 16 20 27 34 raltp 
 |-  ( A. x e. { 0 , 1 , 2 } { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) <-> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) ) )
36 simpr1 
 |-  ( ( ( P ` 0 ) = ( P ` 3 ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) ) ) -> { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) )
37 preq2 
 |-  ( ( P ` 0 ) = ( P ` 3 ) -> { ( P ` 2 ) , ( P ` 0 ) } = { ( P ` 2 ) , ( P ` 3 ) } )
38 prcom 
 |-  { ( P ` 2 ) , ( P ` 0 ) } = { ( P ` 0 ) , ( P ` 2 ) }
39 37 38 eqtr3di 
 |-  ( ( P ` 0 ) = ( P ` 3 ) -> { ( P ` 2 ) , ( P ` 3 ) } = { ( P ` 0 ) , ( P ` 2 ) } )
40 39 eleq1d 
 |-  ( ( P ` 0 ) = ( P ` 3 ) -> ( { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) <-> { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) ) )
41 40 biimpcd 
 |-  ( { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) -> ( ( P ` 0 ) = ( P ` 3 ) -> { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) ) )
42 41 3ad2ant3 
 |-  ( ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) ) -> ( ( P ` 0 ) = ( P ` 3 ) -> { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) ) )
43 42 impcom 
 |-  ( ( ( P ` 0 ) = ( P ` 3 ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) ) ) -> { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) )
44 simpr2 
 |-  ( ( ( P ` 0 ) = ( P ` 3 ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) ) ) -> { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) )
45 36 43 44 3jca 
 |-  ( ( ( P ` 0 ) = ( P ` 3 ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) ) ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) )
46 45 ex 
 |-  ( ( P ` 0 ) = ( P ` 3 ) -> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 2 ) , ( P ` 3 ) } e. ( Edg ` G ) ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) ) )
47 35 46 biimtrid 
 |-  ( ( P ` 0 ) = ( P ` 3 ) -> ( A. x e. { 0 , 1 , 2 } { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) ) )
48 13 47 biimtrdi 
 |-  ( ( # ` F ) = 3 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( A. x e. { 0 , 1 , 2 } { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) ) ) )
49 48 impcom 
 |-  ( ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) -> ( A. x e. { 0 , 1 , 2 } { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) ) )
50 49 adantl 
 |-  ( ( ( G e. UPGraph /\ F ( Paths ` G ) P ) /\ ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) ) -> ( A. x e. { 0 , 1 , 2 } { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) ) )
51 11 50 sylbid 
 |-  ( ( ( G e. UPGraph /\ F ( Paths ` G ) P ) /\ ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ( Edg ` G ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) ) )
52 5 51 mpd 
 |-  ( ( ( G e. UPGraph /\ F ( Paths ` G ) P ) /\ ( ( P ` 0 ) = ( P ` ( # ` F ) ) /\ ( # ` F ) = 3 ) ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) )