Metamath Proof Explorer


Theorem upgr3v3e3cycl

Description: If there is a cycle of length 3 in a pseudograph, there are three distinct vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017)

Ref Expression
Hypotheses upgr3v3e3cycl.e
|- E = ( Edg ` G )
upgr3v3e3cycl.v
|- V = ( Vtx ` G )
Assertion upgr3v3e3cycl
|- ( ( G e. UPGraph /\ F ( Cycles ` G ) P /\ ( # ` F ) = 3 ) -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) )

Proof

Step Hyp Ref Expression
1 upgr3v3e3cycl.e
 |-  E = ( Edg ` G )
2 upgr3v3e3cycl.v
 |-  V = ( Vtx ` G )
3 cyclprop
 |-  ( F ( Cycles ` G ) P -> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
4 pthiswlk
 |-  ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
5 1 upgrwlkvtxedg
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E )
6 fveq2
 |-  ( ( # ` F ) = 3 -> ( P ` ( # ` F ) ) = ( P ` 3 ) )
7 6 eqeq2d
 |-  ( ( # ` F ) = 3 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( P ` 0 ) = ( P ` 3 ) ) )
8 7 anbi2d
 |-  ( ( # ` F ) = 3 -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) ) )
9 oveq2
 |-  ( ( # ` F ) = 3 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 3 ) )
10 fzo0to3tp
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
11 9 10 eqtrdi
 |-  ( ( # ` F ) = 3 -> ( 0 ..^ ( # ` F ) ) = { 0 , 1 , 2 } )
12 11 raleqdv
 |-  ( ( # ` F ) = 3 -> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> A. k e. { 0 , 1 , 2 } { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) )
13 c0ex
 |-  0 e. _V
14 1ex
 |-  1 e. _V
15 2ex
 |-  2 e. _V
16 fveq2
 |-  ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
17 fv0p1e1
 |-  ( k = 0 -> ( P ` ( k + 1 ) ) = ( P ` 1 ) )
18 16 17 preq12d
 |-  ( k = 0 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 0 ) , ( P ` 1 ) } )
19 18 eleq1d
 |-  ( k = 0 -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> { ( P ` 0 ) , ( P ` 1 ) } e. E ) )
20 fveq2
 |-  ( k = 1 -> ( P ` k ) = ( P ` 1 ) )
21 oveq1
 |-  ( k = 1 -> ( k + 1 ) = ( 1 + 1 ) )
22 1p1e2
 |-  ( 1 + 1 ) = 2
23 21 22 eqtrdi
 |-  ( k = 1 -> ( k + 1 ) = 2 )
24 23 fveq2d
 |-  ( k = 1 -> ( P ` ( k + 1 ) ) = ( P ` 2 ) )
25 20 24 preq12d
 |-  ( k = 1 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 1 ) , ( P ` 2 ) } )
26 25 eleq1d
 |-  ( k = 1 -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> { ( P ` 1 ) , ( P ` 2 ) } e. E ) )
27 fveq2
 |-  ( k = 2 -> ( P ` k ) = ( P ` 2 ) )
28 oveq1
 |-  ( k = 2 -> ( k + 1 ) = ( 2 + 1 ) )
29 2p1e3
 |-  ( 2 + 1 ) = 3
30 28 29 eqtrdi
 |-  ( k = 2 -> ( k + 1 ) = 3 )
31 30 fveq2d
 |-  ( k = 2 -> ( P ` ( k + 1 ) ) = ( P ` 3 ) )
32 27 31 preq12d
 |-  ( k = 2 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 2 ) , ( P ` 3 ) } )
33 32 eleq1d
 |-  ( k = 2 -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> { ( P ` 2 ) , ( P ` 3 ) } e. E ) )
34 13 14 15 19 26 33 raltp
 |-  ( A. k e. { 0 , 1 , 2 } { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) )
35 12 34 bitrdi
 |-  ( ( # ` F ) = 3 -> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) )
36 8 35 anbi12d
 |-  ( ( # ` F ) = 3 -> ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) <-> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) ) )
37 2 wlkp
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
38 oveq2
 |-  ( ( # ` F ) = 3 -> ( 0 ... ( # ` F ) ) = ( 0 ... 3 ) )
39 38 feq2d
 |-  ( ( # ` F ) = 3 -> ( P : ( 0 ... ( # ` F ) ) --> V <-> P : ( 0 ... 3 ) --> V ) )
40 id
 |-  ( P : ( 0 ... 3 ) --> V -> P : ( 0 ... 3 ) --> V )
41 3nn0
 |-  3 e. NN0
42 0elfz
 |-  ( 3 e. NN0 -> 0 e. ( 0 ... 3 ) )
43 41 42 mp1i
 |-  ( P : ( 0 ... 3 ) --> V -> 0 e. ( 0 ... 3 ) )
44 40 43 ffvelrnd
 |-  ( P : ( 0 ... 3 ) --> V -> ( P ` 0 ) e. V )
45 1nn0
 |-  1 e. NN0
46 1lt3
 |-  1 < 3
47 fvffz0
 |-  ( ( ( 3 e. NN0 /\ 1 e. NN0 /\ 1 < 3 ) /\ P : ( 0 ... 3 ) --> V ) -> ( P ` 1 ) e. V )
48 47 ex
 |-  ( ( 3 e. NN0 /\ 1 e. NN0 /\ 1 < 3 ) -> ( P : ( 0 ... 3 ) --> V -> ( P ` 1 ) e. V ) )
49 41 45 46 48 mp3an
 |-  ( P : ( 0 ... 3 ) --> V -> ( P ` 1 ) e. V )
50 2nn0
 |-  2 e. NN0
51 2lt3
 |-  2 < 3
52 fvffz0
 |-  ( ( ( 3 e. NN0 /\ 2 e. NN0 /\ 2 < 3 ) /\ P : ( 0 ... 3 ) --> V ) -> ( P ` 2 ) e. V )
53 52 ex
 |-  ( ( 3 e. NN0 /\ 2 e. NN0 /\ 2 < 3 ) -> ( P : ( 0 ... 3 ) --> V -> ( P ` 2 ) e. V ) )
54 41 50 51 53 mp3an
 |-  ( P : ( 0 ... 3 ) --> V -> ( P ` 2 ) e. V )
55 44 49 54 3jca
 |-  ( P : ( 0 ... 3 ) --> V -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) )
56 39 55 syl6bi
 |-  ( ( # ` F ) = 3 -> ( P : ( 0 ... ( # ` F ) ) --> V -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) ) )
57 56 com12
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) ) )
58 4 37 57 3syl
 |-  ( F ( Paths ` G ) P -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) ) )
59 58 adantr
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) ) )
60 59 adantr
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) ) )
61 60 impcom
 |-  ( ( ( # ` F ) = 3 /\ ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) ) -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) )
62 preq2
 |-  ( ( P ` 3 ) = ( P ` 0 ) -> { ( P ` 2 ) , ( P ` 3 ) } = { ( P ` 2 ) , ( P ` 0 ) } )
63 62 eqcoms
 |-  ( ( P ` 0 ) = ( P ` 3 ) -> { ( P ` 2 ) , ( P ` 3 ) } = { ( P ` 2 ) , ( P ` 0 ) } )
64 63 adantl
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) -> { ( P ` 2 ) , ( P ` 3 ) } = { ( P ` 2 ) , ( P ` 0 ) } )
65 64 eleq1d
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) -> ( { ( P ` 2 ) , ( P ` 3 ) } e. E <-> { ( P ` 2 ) , ( P ` 0 ) } e. E ) )
66 65 3anbi3d
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) -> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) <-> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 0 ) } e. E ) ) )
67 66 biimpa
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 0 ) } e. E ) )
68 67 adantl
 |-  ( ( ( # ` F ) = 3 /\ ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 0 ) } e. E ) )
69 simpll
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> F ( Paths ` G ) P )
70 breq2
 |-  ( ( # ` F ) = 3 -> ( 1 < ( # ` F ) <-> 1 < 3 ) )
71 46 70 mpbiri
 |-  ( ( # ` F ) = 3 -> 1 < ( # ` F ) )
72 71 adantl
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> 1 < ( # ` F ) )
73 3nn
 |-  3 e. NN
74 lbfzo0
 |-  ( 0 e. ( 0 ..^ 3 ) <-> 3 e. NN )
75 73 74 mpbir
 |-  0 e. ( 0 ..^ 3 )
76 75 9 eleqtrrid
 |-  ( ( # ` F ) = 3 -> 0 e. ( 0 ..^ ( # ` F ) ) )
77 76 adantl
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
78 pthdadjvtx
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ 0 e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` 0 ) =/= ( P ` ( 0 + 1 ) ) )
79 1e0p1
 |-  1 = ( 0 + 1 )
80 79 fveq2i
 |-  ( P ` 1 ) = ( P ` ( 0 + 1 ) )
81 80 neeq2i
 |-  ( ( P ` 0 ) =/= ( P ` 1 ) <-> ( P ` 0 ) =/= ( P ` ( 0 + 1 ) ) )
82 78 81 sylibr
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ 0 e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` 0 ) =/= ( P ` 1 ) )
83 69 72 77 82 syl3anc
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> ( P ` 0 ) =/= ( P ` 1 ) )
84 elfzo0
 |-  ( 1 e. ( 0 ..^ 3 ) <-> ( 1 e. NN0 /\ 3 e. NN /\ 1 < 3 ) )
85 45 73 46 84 mpbir3an
 |-  1 e. ( 0 ..^ 3 )
86 85 9 eleqtrrid
 |-  ( ( # ` F ) = 3 -> 1 e. ( 0 ..^ ( # ` F ) ) )
87 86 adantl
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> 1 e. ( 0 ..^ ( # ` F ) ) )
88 pthdadjvtx
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ 1 e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` 1 ) =/= ( P ` ( 1 + 1 ) ) )
89 df-2
 |-  2 = ( 1 + 1 )
90 89 fveq2i
 |-  ( P ` 2 ) = ( P ` ( 1 + 1 ) )
91 90 neeq2i
 |-  ( ( P ` 1 ) =/= ( P ` 2 ) <-> ( P ` 1 ) =/= ( P ` ( 1 + 1 ) ) )
92 88 91 sylibr
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ 1 e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` 1 ) =/= ( P ` 2 ) )
93 69 72 87 92 syl3anc
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> ( P ` 1 ) =/= ( P ` 2 ) )
94 elfzo0
 |-  ( 2 e. ( 0 ..^ 3 ) <-> ( 2 e. NN0 /\ 3 e. NN /\ 2 < 3 ) )
95 50 73 51 94 mpbir3an
 |-  2 e. ( 0 ..^ 3 )
96 95 9 eleqtrrid
 |-  ( ( # ` F ) = 3 -> 2 e. ( 0 ..^ ( # ` F ) ) )
97 96 adantl
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> 2 e. ( 0 ..^ ( # ` F ) ) )
98 pthdadjvtx
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ 2 e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` 2 ) =/= ( P ` ( 2 + 1 ) ) )
99 69 72 97 98 syl3anc
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> ( P ` 2 ) =/= ( P ` ( 2 + 1 ) ) )
100 neeq2
 |-  ( ( P ` 0 ) = ( P ` 3 ) -> ( ( P ` 2 ) =/= ( P ` 0 ) <-> ( P ` 2 ) =/= ( P ` 3 ) ) )
101 df-3
 |-  3 = ( 2 + 1 )
102 101 fveq2i
 |-  ( P ` 3 ) = ( P ` ( 2 + 1 ) )
103 102 neeq2i
 |-  ( ( P ` 2 ) =/= ( P ` 3 ) <-> ( P ` 2 ) =/= ( P ` ( 2 + 1 ) ) )
104 100 103 bitrdi
 |-  ( ( P ` 0 ) = ( P ` 3 ) -> ( ( P ` 2 ) =/= ( P ` 0 ) <-> ( P ` 2 ) =/= ( P ` ( 2 + 1 ) ) ) )
105 104 adantl
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) -> ( ( P ` 2 ) =/= ( P ` 0 ) <-> ( P ` 2 ) =/= ( P ` ( 2 + 1 ) ) ) )
106 105 adantr
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> ( ( P ` 2 ) =/= ( P ` 0 ) <-> ( P ` 2 ) =/= ( P ` ( 2 + 1 ) ) ) )
107 99 106 mpbird
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> ( P ` 2 ) =/= ( P ` 0 ) )
108 83 93 107 3jca
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( # ` F ) = 3 ) -> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 2 ) =/= ( P ` 0 ) ) )
109 108 ex
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 2 ) =/= ( P ` 0 ) ) ) )
110 109 adantr
 |-  ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) -> ( ( # ` F ) = 3 -> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 2 ) =/= ( P ` 0 ) ) ) )
111 110 impcom
 |-  ( ( ( # ` F ) = 3 /\ ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) ) -> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 2 ) =/= ( P ` 0 ) ) )
112 preq1
 |-  ( a = ( P ` 0 ) -> { a , b } = { ( P ` 0 ) , b } )
113 112 eleq1d
 |-  ( a = ( P ` 0 ) -> ( { a , b } e. E <-> { ( P ` 0 ) , b } e. E ) )
114 preq2
 |-  ( a = ( P ` 0 ) -> { c , a } = { c , ( P ` 0 ) } )
115 114 eleq1d
 |-  ( a = ( P ` 0 ) -> ( { c , a } e. E <-> { c , ( P ` 0 ) } e. E ) )
116 113 115 3anbi13d
 |-  ( a = ( P ` 0 ) -> ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) <-> ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E /\ { c , ( P ` 0 ) } e. E ) ) )
117 neeq1
 |-  ( a = ( P ` 0 ) -> ( a =/= b <-> ( P ` 0 ) =/= b ) )
118 neeq2
 |-  ( a = ( P ` 0 ) -> ( c =/= a <-> c =/= ( P ` 0 ) ) )
119 117 118 3anbi13d
 |-  ( a = ( P ` 0 ) -> ( ( a =/= b /\ b =/= c /\ c =/= a ) <-> ( ( P ` 0 ) =/= b /\ b =/= c /\ c =/= ( P ` 0 ) ) ) )
120 116 119 anbi12d
 |-  ( a = ( P ` 0 ) -> ( ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) <-> ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E /\ { c , ( P ` 0 ) } e. E ) /\ ( ( P ` 0 ) =/= b /\ b =/= c /\ c =/= ( P ` 0 ) ) ) ) )
121 preq2
 |-  ( b = ( P ` 1 ) -> { ( P ` 0 ) , b } = { ( P ` 0 ) , ( P ` 1 ) } )
122 121 eleq1d
 |-  ( b = ( P ` 1 ) -> ( { ( P ` 0 ) , b } e. E <-> { ( P ` 0 ) , ( P ` 1 ) } e. E ) )
123 preq1
 |-  ( b = ( P ` 1 ) -> { b , c } = { ( P ` 1 ) , c } )
124 123 eleq1d
 |-  ( b = ( P ` 1 ) -> ( { b , c } e. E <-> { ( P ` 1 ) , c } e. E ) )
125 122 124 3anbi12d
 |-  ( b = ( P ` 1 ) -> ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E /\ { c , ( P ` 0 ) } e. E ) <-> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E /\ { c , ( P ` 0 ) } e. E ) ) )
126 neeq2
 |-  ( b = ( P ` 1 ) -> ( ( P ` 0 ) =/= b <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
127 neeq1
 |-  ( b = ( P ` 1 ) -> ( b =/= c <-> ( P ` 1 ) =/= c ) )
128 126 127 3anbi12d
 |-  ( b = ( P ` 1 ) -> ( ( ( P ` 0 ) =/= b /\ b =/= c /\ c =/= ( P ` 0 ) ) <-> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= c /\ c =/= ( P ` 0 ) ) ) )
129 125 128 anbi12d
 |-  ( b = ( P ` 1 ) -> ( ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E /\ { c , ( P ` 0 ) } e. E ) /\ ( ( P ` 0 ) =/= b /\ b =/= c /\ c =/= ( P ` 0 ) ) ) <-> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E /\ { c , ( P ` 0 ) } e. E ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= c /\ c =/= ( P ` 0 ) ) ) ) )
130 preq2
 |-  ( c = ( P ` 2 ) -> { ( P ` 1 ) , c } = { ( P ` 1 ) , ( P ` 2 ) } )
131 130 eleq1d
 |-  ( c = ( P ` 2 ) -> ( { ( P ` 1 ) , c } e. E <-> { ( P ` 1 ) , ( P ` 2 ) } e. E ) )
132 preq1
 |-  ( c = ( P ` 2 ) -> { c , ( P ` 0 ) } = { ( P ` 2 ) , ( P ` 0 ) } )
133 132 eleq1d
 |-  ( c = ( P ` 2 ) -> ( { c , ( P ` 0 ) } e. E <-> { ( P ` 2 ) , ( P ` 0 ) } e. E ) )
134 131 133 3anbi23d
 |-  ( c = ( P ` 2 ) -> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E /\ { c , ( P ` 0 ) } e. E ) <-> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 0 ) } e. E ) ) )
135 neeq2
 |-  ( c = ( P ` 2 ) -> ( ( P ` 1 ) =/= c <-> ( P ` 1 ) =/= ( P ` 2 ) ) )
136 neeq1
 |-  ( c = ( P ` 2 ) -> ( c =/= ( P ` 0 ) <-> ( P ` 2 ) =/= ( P ` 0 ) ) )
137 135 136 3anbi23d
 |-  ( c = ( P ` 2 ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= c /\ c =/= ( P ` 0 ) ) <-> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 2 ) =/= ( P ` 0 ) ) ) )
138 134 137 anbi12d
 |-  ( c = ( P ` 2 ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E /\ { c , ( P ` 0 ) } e. E ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= c /\ c =/= ( P ` 0 ) ) ) <-> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 0 ) } e. E ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 2 ) =/= ( P ` 0 ) ) ) ) )
139 120 129 138 rspc3ev
 |-  ( ( ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ ( P ` 2 ) e. V ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 0 ) } e. E ) /\ ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 2 ) =/= ( P ` 0 ) ) ) ) -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) )
140 61 68 111 139 syl12anc
 |-  ( ( ( # ` F ) = 3 /\ ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) ) -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) )
141 140 ex
 |-  ( ( # ` F ) = 3 -> ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 3 ) ) /\ ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E /\ { ( P ` 2 ) , ( P ` 3 ) } e. E ) ) -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) )
142 36 141 sylbid
 |-  ( ( # ` F ) = 3 -> ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) )
143 142 expd
 |-  ( ( # ` F ) = 3 -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) ) )
144 143 com13
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 3 -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) ) )
145 5 144 syl
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 3 -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) ) )
146 145 expcom
 |-  ( F ( Walks ` G ) P -> ( G e. UPGraph -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 3 -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) ) ) )
147 146 com23
 |-  ( F ( Walks ` G ) P -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( G e. UPGraph -> ( ( # ` F ) = 3 -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) ) ) )
148 147 expd
 |-  ( F ( Walks ` G ) P -> ( F ( Paths ` G ) P -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( G e. UPGraph -> ( ( # ` F ) = 3 -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) ) ) ) )
149 4 148 mpcom
 |-  ( F ( Paths ` G ) P -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( G e. UPGraph -> ( ( # ` F ) = 3 -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) ) ) )
150 149 imp
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( G e. UPGraph -> ( ( # ` F ) = 3 -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) ) )
151 3 150 syl
 |-  ( F ( Cycles ` G ) P -> ( G e. UPGraph -> ( ( # ` F ) = 3 -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) ) ) )
152 151 3imp21
 |-  ( ( G e. UPGraph /\ F ( Cycles ` G ) P /\ ( # ` F ) = 3 ) -> E. a e. V E. b e. V E. c e. V ( ( { a , b } e. E /\ { b , c } e. E /\ { c , a } e. E ) /\ ( a =/= b /\ b =/= c /\ c =/= a ) ) )