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

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 ffvelcdmd 
 |-  ( 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 biimtrdi 
 |-  ( ( # ` 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 ) ) )