Metamath Proof Explorer

Theorem upgr4cycl4dv4e

Description: If there is a cycle of length 4 in a pseudograph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017) (Revised by AV, 13-Feb-2021)

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

Proof

Step Hyp Ref Expression
1 upgr4cycl4dv4e.v 
 |-  V = ( Vtx ` G )
2 upgr4cycl4dv4e.e 
 |-  E = ( Edg ` 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 2 upgrwlkvtxedg 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E )
6 fveq2 
 |-  ( ( # ` F ) = 4 -> ( P ` ( # ` F ) ) = ( P ` 4 ) )
7 6 eqeq2d 
 |-  ( ( # ` F ) = 4 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( P ` 0 ) = ( P ` 4 ) ) )
8 7 anbi2d 
 |-  ( ( # ` F ) = 4 -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 4 ) ) ) )
9 oveq2 
 |-  ( ( # ` F ) = 4 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) )
10 fzo0to42pr 
 |-  ( 0 ..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } )
11 9 10 eqtrdi 
 |-  ( ( # ` F ) = 4 -> ( 0 ..^ ( # ` F ) ) = ( { 0 , 1 } u. { 2 , 3 } ) )
12 11 raleqdv 
 |-  ( ( # ` F ) = 4 -> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> A. k e. ( { 0 , 1 } u. { 2 , 3 } ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) )
13 ralunb 
 |-  ( A. k e. ( { 0 , 1 } u. { 2 , 3 } ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> ( A. k e. { 0 , 1 } { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E /\ A. k e. { 2 , 3 } { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E ) )
14 c0ex 
 |-  0 e. _V
15 1ex 
 |-  1 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 14 15 19 26 ralpr 
 |-  ( A. k e. { 0 , 1 } { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) )
28 2ex 
 |-  2 e. _V
29 3ex 
 |-  3 e. _V
30 fveq2 
 |-  ( k = 2 -> ( P ` k ) = ( P ` 2 ) )
31 oveq1 
 |-  ( k = 2 -> ( k + 1 ) = ( 2 + 1 ) )
32 2p1e3 
 |-  ( 2 + 1 ) = 3
33 31 32 eqtrdi 
 |-  ( k = 2 -> ( k + 1 ) = 3 )
34 33 fveq2d 
 |-  ( k = 2 -> ( P ` ( k + 1 ) ) = ( P ` 3 ) )
35 30 34 preq12d 
 |-  ( k = 2 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 2 ) , ( P ` 3 ) } )
36 35 eleq1d 
 |-  ( k = 2 -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> { ( P ` 2 ) , ( P ` 3 ) } e. E ) )
37 fveq2 
 |-  ( k = 3 -> ( P ` k ) = ( P ` 3 ) )
38 oveq1 
 |-  ( k = 3 -> ( k + 1 ) = ( 3 + 1 ) )
39 3p1e4 
 |-  ( 3 + 1 ) = 4
40 38 39 eqtrdi 
 |-  ( k = 3 -> ( k + 1 ) = 4 )
41 40 fveq2d 
 |-  ( k = 3 -> ( P ` ( k + 1 ) ) = ( P ` 4 ) )
42 37 41 preq12d 
 |-  ( k = 3 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 3 ) , ( P ` 4 ) } )
43 42 eleq1d 
 |-  ( k = 3 -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> { ( P ` 3 ) , ( P ` 4 ) } e. E ) )
44 28 29 36 43 ralpr 
 |-  ( A. k e. { 2 , 3 } { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E <-> ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) )
45 27 44 anbi12i 
 |-  ( ( A. k e. { 0 , 1 } { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E /\ A. k e. { 2 , 3 } { ( 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 /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) )
46 13 45 bitri 
 |-  ( A. k e. ( { 0 , 1 } u. { 2 , 3 } ) { ( 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 /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) )
47 12 46 bitrdi 
 |-  ( ( # ` F ) = 4 -> ( 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 /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) ) )
48 8 47 anbi12d 
 |-  ( ( # ` F ) = 4 -> ( ( ( 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 ` 4 ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) ) ) )
49 preq2 
 |-  ( ( P ` 4 ) = ( P ` 0 ) -> { ( P ` 3 ) , ( P ` 4 ) } = { ( P ` 3 ) , ( P ` 0 ) } )
50 49 eleq1d 
 |-  ( ( P ` 4 ) = ( P ` 0 ) -> ( { ( P ` 3 ) , ( P ` 4 ) } e. E <-> { ( P ` 3 ) , ( P ` 0 ) } e. E ) )
51 50 eqcoms 
 |-  ( ( P ` 0 ) = ( P ` 4 ) -> ( { ( P ` 3 ) , ( P ` 4 ) } e. E <-> { ( P ` 3 ) , ( P ` 0 ) } e. E ) )
52 51 anbi2d 
 |-  ( ( P ` 0 ) = ( P ` 4 ) -> ( ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) <-> ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) )
53 52 anbi2d 
 |-  ( ( P ` 0 ) = ( P ` 4 ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) <-> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) )
54 53 adantl 
 |-  ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( P ` 0 ) = ( P ` 4 ) ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) <-> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) )
55 4nn0 
 |-  4 e. NN0
56 55 a1i 
 |-  ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) -> 4 e. NN0 )
57 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
58 oveq2 
 |-  ( ( # ` F ) = 4 -> ( 0 ... ( # ` F ) ) = ( 0 ... 4 ) )
59 58 feq2d 
 |-  ( ( # ` F ) = 4 -> ( P : ( 0 ... ( # ` F ) ) --> V <-> P : ( 0 ... 4 ) --> V ) )
60 59 biimpcd 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> ( ( # ` F ) = 4 -> P : ( 0 ... 4 ) --> V ) )
61 4 57 60 3syl 
 |-  ( F ( Paths ` G ) P -> ( ( # ` F ) = 4 -> P : ( 0 ... 4 ) --> V ) )
62 61 impcom 
 |-  ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) -> P : ( 0 ... 4 ) --> V )
63 id 
 |-  ( 4 e. NN0 -> 4 e. NN0 )
64 0nn0 
 |-  0 e. NN0
65 64 a1i 
 |-  ( 4 e. NN0 -> 0 e. NN0 )
66 4pos 
 |-  0 < 4
67 66 a1i 
 |-  ( 4 e. NN0 -> 0 < 4 )
68 63 65 67 3jca 
 |-  ( 4 e. NN0 -> ( 4 e. NN0 /\ 0 e. NN0 /\ 0 < 4 ) )
69 fvffz0 
 |-  ( ( ( 4 e. NN0 /\ 0 e. NN0 /\ 0 < 4 ) /\ P : ( 0 ... 4 ) --> V ) -> ( P ` 0 ) e. V )
70 68 69 sylan 
 |-  ( ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) -> ( P ` 0 ) e. V )
71 70 ad2antlr 
 |-  ( ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) -> ( P ` 0 ) e. V )
72 1nn0 
 |-  1 e. NN0
73 72 a1i 
 |-  ( 4 e. NN0 -> 1 e. NN0 )
74 1lt4 
 |-  1 < 4
75 74 a1i 
 |-  ( 4 e. NN0 -> 1 < 4 )
76 63 73 75 3jca 
 |-  ( 4 e. NN0 -> ( 4 e. NN0 /\ 1 e. NN0 /\ 1 < 4 ) )
77 fvffz0 
 |-  ( ( ( 4 e. NN0 /\ 1 e. NN0 /\ 1 < 4 ) /\ P : ( 0 ... 4 ) --> V ) -> ( P ` 1 ) e. V )
78 76 77 sylan 
 |-  ( ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) -> ( P ` 1 ) e. V )
79 78 ad2antlr 
 |-  ( ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) -> ( P ` 1 ) e. V )
80 2nn0 
 |-  2 e. NN0
81 80 a1i 
 |-  ( 4 e. NN0 -> 2 e. NN0 )
82 2lt4 
 |-  2 < 4
83 82 a1i 
 |-  ( 4 e. NN0 -> 2 < 4 )
84 63 81 83 3jca 
 |-  ( 4 e. NN0 -> ( 4 e. NN0 /\ 2 e. NN0 /\ 2 < 4 ) )
85 fvffz0 
 |-  ( ( ( 4 e. NN0 /\ 2 e. NN0 /\ 2 < 4 ) /\ P : ( 0 ... 4 ) --> V ) -> ( P ` 2 ) e. V )
86 84 85 sylan 
 |-  ( ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) -> ( P ` 2 ) e. V )
87 86 ad2antlr 
 |-  ( ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) -> ( P ` 2 ) e. V )
88 3nn0 
 |-  3 e. NN0
89 88 a1i 
 |-  ( 4 e. NN0 -> 3 e. NN0 )
90 3lt4 
 |-  3 < 4
91 90 a1i 
 |-  ( 4 e. NN0 -> 3 < 4 )
92 63 89 91 3jca 
 |-  ( 4 e. NN0 -> ( 4 e. NN0 /\ 3 e. NN0 /\ 3 < 4 ) )
93 fvffz0 
 |-  ( ( ( 4 e. NN0 /\ 3 e. NN0 /\ 3 < 4 ) /\ P : ( 0 ... 4 ) --> V ) -> ( P ` 3 ) e. V )
94 92 93 sylan 
 |-  ( ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) -> ( P ` 3 ) e. V )
95 94 ad2antlr 
 |-  ( ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) -> ( P ` 3 ) e. V )
96 simpr 
 |-  ( ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) -> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) )
97 simplr 
 |-  ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) -> F ( Paths ` G ) P )
98 breq2 
 |-  ( ( # ` F ) = 4 -> ( 1 < ( # ` F ) <-> 1 < 4 ) )
99 74 98 mpbiri 
 |-  ( ( # ` F ) = 4 -> 1 < ( # ` F ) )
100 99 ad2antrr 
 |-  ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) -> 1 < ( # ` F ) )
101 simpll 
 |-  ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) -> ( # ` F ) = 4 )
102 9 ad2antrr 
 |-  ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) )
103 4nn 
 |-  4 e. NN
104 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 4 ) <-> 4 e. NN )
105 103 104 mpbir 
 |-  0 e. ( 0 ..^ 4 )
106 eleq2 
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) -> ( 0 e. ( 0 ..^ ( # ` F ) ) <-> 0 e. ( 0 ..^ 4 ) ) )
107 105 106 mpbiri 
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
108 107 adantl 
 |-  ( ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
109 pthdadjvtx 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ 0 e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` 0 ) =/= ( P ` ( 0 + 1 ) ) )
110 108 109 syl3an3 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 0 ) =/= ( P ` ( 0 + 1 ) ) )
111 1e0p1 
 |-  1 = ( 0 + 1 )
112 111 fveq2i 
 |-  ( P ` 1 ) = ( P ` ( 0 + 1 ) )
113 112 neeq2i 
 |-  ( ( P ` 0 ) =/= ( P ` 1 ) <-> ( P ` 0 ) =/= ( P ` ( 0 + 1 ) ) )
114 110 113 sylibr 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 0 ) =/= ( P ` 1 ) )
115 simp1 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> F ( Paths ` G ) P )
116 elfzo0 
 |-  ( 2 e. ( 0 ..^ 4 ) <-> ( 2 e. NN0 /\ 4 e. NN /\ 2 < 4 ) )
117 80 103 82 116 mpbir3an 
 |-  2 e. ( 0 ..^ 4 )
118 2ne0 
 |-  2 =/= 0
119 fzo1fzo0n0 
 |-  ( 2 e. ( 1 ..^ 4 ) <-> ( 2 e. ( 0 ..^ 4 ) /\ 2 =/= 0 ) )
120 117 118 119 mpbir2an 
 |-  2 e. ( 1 ..^ 4 )
121 oveq2 
 |-  ( ( # ` F ) = 4 -> ( 1 ..^ ( # ` F ) ) = ( 1 ..^ 4 ) )
122 120 121 eleqtrrid 
 |-  ( ( # ` F ) = 4 -> 2 e. ( 1 ..^ ( # ` F ) ) )
123 0elfz 
 |-  ( 4 e. NN0 -> 0 e. ( 0 ... 4 ) )
124 55 123 ax-mp 
 |-  0 e. ( 0 ... 4 )
125 124 58 eleqtrrid 
 |-  ( ( # ` F ) = 4 -> 0 e. ( 0 ... ( # ` F ) ) )
126 118 a1i 
 |-  ( ( # ` F ) = 4 -> 2 =/= 0 )
127 122 125 126 3jca 
 |-  ( ( # ` F ) = 4 -> ( 2 e. ( 1 ..^ ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ 2 =/= 0 ) )
128 127 adantr 
 |-  ( ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) -> ( 2 e. ( 1 ..^ ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ 2 =/= 0 ) )
129 128 3ad2ant3 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( 2 e. ( 1 ..^ ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ 2 =/= 0 ) )
130 pthdivtx 
 |-  ( ( F ( Paths ` G ) P /\ ( 2 e. ( 1 ..^ ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ 2 =/= 0 ) ) -> ( P ` 2 ) =/= ( P ` 0 ) )
131 115 129 130 syl2anc 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 2 ) =/= ( P ` 0 ) )
132 131 necomd 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 0 ) =/= ( P ` 2 ) )
133 elfzo0 
 |-  ( 3 e. ( 0 ..^ 4 ) <-> ( 3 e. NN0 /\ 4 e. NN /\ 3 < 4 ) )
134 88 103 90 133 mpbir3an 
 |-  3 e. ( 0 ..^ 4 )
135 3ne0 
 |-  3 =/= 0
136 fzo1fzo0n0 
 |-  ( 3 e. ( 1 ..^ 4 ) <-> ( 3 e. ( 0 ..^ 4 ) /\ 3 =/= 0 ) )
137 134 135 136 mpbir2an 
 |-  3 e. ( 1 ..^ 4 )
138 137 121 eleqtrrid 
 |-  ( ( # ` F ) = 4 -> 3 e. ( 1 ..^ ( # ` F ) ) )
139 135 a1i 
 |-  ( ( # ` F ) = 4 -> 3 =/= 0 )
140 138 125 139 3jca 
 |-  ( ( # ` F ) = 4 -> ( 3 e. ( 1 ..^ ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ 3 =/= 0 ) )
141 140 adantr 
 |-  ( ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) -> ( 3 e. ( 1 ..^ ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ 3 =/= 0 ) )
142 141 3ad2ant3 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( 3 e. ( 1 ..^ ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ 3 =/= 0 ) )
143 pthdivtx 
 |-  ( ( F ( Paths ` G ) P /\ ( 3 e. ( 1 ..^ ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ 3 =/= 0 ) ) -> ( P ` 3 ) =/= ( P ` 0 ) )
144 115 142 143 syl2anc 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 3 ) =/= ( P ` 0 ) )
145 144 necomd 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 0 ) =/= ( P ` 3 ) )
146 114 132 145 3jca 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= ( P ` 3 ) ) )
147 elfzo0 
 |-  ( 1 e. ( 0 ..^ 4 ) <-> ( 1 e. NN0 /\ 4 e. NN /\ 1 < 4 ) )
148 72 103 74 147 mpbir3an 
 |-  1 e. ( 0 ..^ 4 )
149 eleq2 
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) -> ( 1 e. ( 0 ..^ ( # ` F ) ) <-> 1 e. ( 0 ..^ 4 ) ) )
150 148 149 mpbiri 
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) -> 1 e. ( 0 ..^ ( # ` F ) ) )
151 150 adantl 
 |-  ( ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) -> 1 e. ( 0 ..^ ( # ` F ) ) )
152 pthdadjvtx 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ 1 e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` 1 ) =/= ( P ` ( 1 + 1 ) ) )
153 151 152 syl3an3 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 1 ) =/= ( P ` ( 1 + 1 ) ) )
154 df-2 
 |-  2 = ( 1 + 1 )
155 154 fveq2i 
 |-  ( P ` 2 ) = ( P ` ( 1 + 1 ) )
156 155 neeq2i 
 |-  ( ( P ` 1 ) =/= ( P ` 2 ) <-> ( P ` 1 ) =/= ( P ` ( 1 + 1 ) ) )
157 153 156 sylibr 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 1 ) =/= ( P ` 2 ) )
158 ax-1ne0 
 |-  1 =/= 0
159 fzo1fzo0n0 
 |-  ( 1 e. ( 1 ..^ 4 ) <-> ( 1 e. ( 0 ..^ 4 ) /\ 1 =/= 0 ) )
160 148 158 159 mpbir2an 
 |-  1 e. ( 1 ..^ 4 )
161 160 121 eleqtrrid 
 |-  ( ( # ` F ) = 4 -> 1 e. ( 1 ..^ ( # ` F ) ) )
162 3re 
 |-  3 e. RR
163 4re 
 |-  4 e. RR
164 162 163 90 ltleii 
 |-  3 <_ 4
165 elfz2nn0 
 |-  ( 3 e. ( 0 ... 4 ) <-> ( 3 e. NN0 /\ 4 e. NN0 /\ 3 <_ 4 ) )
166 88 55 164 165 mpbir3an 
 |-  3 e. ( 0 ... 4 )
167 166 58 eleqtrrid 
 |-  ( ( # ` F ) = 4 -> 3 e. ( 0 ... ( # ` F ) ) )
168 1re 
 |-  1 e. RR
169 1lt3 
 |-  1 < 3
170 168 169 ltneii 
 |-  1 =/= 3
171 170 a1i 
 |-  ( ( # ` F ) = 4 -> 1 =/= 3 )
172 161 167 171 3jca 
 |-  ( ( # ` F ) = 4 -> ( 1 e. ( 1 ..^ ( # ` F ) ) /\ 3 e. ( 0 ... ( # ` F ) ) /\ 1 =/= 3 ) )
173 172 adantr 
 |-  ( ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) -> ( 1 e. ( 1 ..^ ( # ` F ) ) /\ 3 e. ( 0 ... ( # ` F ) ) /\ 1 =/= 3 ) )
174 173 3ad2ant3 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( 1 e. ( 1 ..^ ( # ` F ) ) /\ 3 e. ( 0 ... ( # ` F ) ) /\ 1 =/= 3 ) )
175 pthdivtx 
 |-  ( ( F ( Paths ` G ) P /\ ( 1 e. ( 1 ..^ ( # ` F ) ) /\ 3 e. ( 0 ... ( # ` F ) ) /\ 1 =/= 3 ) ) -> ( P ` 1 ) =/= ( P ` 3 ) )
176 115 174 175 syl2anc 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 1 ) =/= ( P ` 3 ) )
177 eleq2 
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) -> ( 2 e. ( 0 ..^ ( # ` F ) ) <-> 2 e. ( 0 ..^ 4 ) ) )
178 117 177 mpbiri 
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) -> 2 e. ( 0 ..^ ( # ` F ) ) )
179 178 adantl 
 |-  ( ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) -> 2 e. ( 0 ..^ ( # ` F ) ) )
180 pthdadjvtx 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ 2 e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` 2 ) =/= ( P ` ( 2 + 1 ) ) )
181 179 180 syl3an3 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 2 ) =/= ( P ` ( 2 + 1 ) ) )
182 df-3 
 |-  3 = ( 2 + 1 )
183 182 fveq2i 
 |-  ( P ` 3 ) = ( P ` ( 2 + 1 ) )
184 183 neeq2i 
 |-  ( ( P ` 2 ) =/= ( P ` 3 ) <-> ( P ` 2 ) =/= ( P ` ( 2 + 1 ) ) )
185 181 184 sylibr 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( P ` 2 ) =/= ( P ` 3 ) )
186 157 176 185 3jca 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 3 ) /\ ( P ` 2 ) =/= ( P ` 3 ) ) )
187 146 186 jca 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ ( ( # ` F ) = 4 /\ ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 4 ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= ( P ` 3 ) ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 3 ) /\ ( P ` 2 ) =/= ( P ` 3 ) ) ) )
188 97 100 101 102 187 syl112anc 
 |-  ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= ( P ` 3 ) ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 3 ) /\ ( P ` 2 ) =/= ( P ` 3 ) ) ) )
189 188 adantr 
 |-  ( ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= ( P ` 3 ) ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 3 ) /\ ( P ` 2 ) =/= ( P ` 3 ) ) ) )
190 preq2 
 |-  ( c = ( P ` 2 ) -> { ( P ` 1 ) , c } = { ( P ` 1 ) , ( P ` 2 ) } )
191 190 eleq1d 
 |-  ( c = ( P ` 2 ) -> ( { ( P ` 1 ) , c } e. E <-> { ( P ` 1 ) , ( P ` 2 ) } e. E ) )
192 191 anbi2d 
 |-  ( c = ( P ` 2 ) -> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) <-> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) ) )
193 preq1 
 |-  ( c = ( P ` 2 ) -> { c , d } = { ( P ` 2 ) , d } )
194 193 eleq1d 
 |-  ( c = ( P ` 2 ) -> ( { c , d } e. E <-> { ( P ` 2 ) , d } e. E ) )
195 194 anbi1d 
 |-  ( c = ( P ` 2 ) -> ( ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) <-> ( { ( P ` 2 ) , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) )
196 192 195 anbi12d 
 |-  ( c = ( P ` 2 ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) <-> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) ) )
197 neeq2 
 |-  ( c = ( P ` 2 ) -> ( ( P ` 0 ) =/= c <-> ( P ` 0 ) =/= ( P ` 2 ) ) )
198 197 3anbi2d 
 |-  ( c = ( P ` 2 ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) <-> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= d ) ) )
199 neeq2 
 |-  ( c = ( P ` 2 ) -> ( ( P ` 1 ) =/= c <-> ( P ` 1 ) =/= ( P ` 2 ) ) )
200 neeq1 
 |-  ( c = ( P ` 2 ) -> ( c =/= d <-> ( P ` 2 ) =/= d ) )
201 199 200 3anbi13d 
 |-  ( c = ( P ` 2 ) -> ( ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) <-> ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= d /\ ( P ` 2 ) =/= d ) ) )
202 198 201 anbi12d 
 |-  ( c = ( P ` 2 ) -> ( ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) <-> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= d /\ ( P ` 2 ) =/= d ) ) ) )
203 196 202 anbi12d 
 |-  ( c = ( P ` 2 ) -> ( ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) <-> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= d /\ ( P ` 2 ) =/= d ) ) ) ) )
204 preq2 
 |-  ( d = ( P ` 3 ) -> { ( P ` 2 ) , d } = { ( P ` 2 ) , ( P ` 3 ) } )
205 204 eleq1d 
 |-  ( d = ( P ` 3 ) -> ( { ( P ` 2 ) , d } e. E <-> { ( P ` 2 ) , ( P ` 3 ) } e. E ) )
206 preq1 
 |-  ( d = ( P ` 3 ) -> { d , ( P ` 0 ) } = { ( P ` 3 ) , ( P ` 0 ) } )
207 206 eleq1d 
 |-  ( d = ( P ` 3 ) -> ( { d , ( P ` 0 ) } e. E <-> { ( P ` 3 ) , ( P ` 0 ) } e. E ) )
208 205 207 anbi12d 
 |-  ( d = ( P ` 3 ) -> ( ( { ( P ` 2 ) , d } e. E /\ { d , ( P ` 0 ) } e. E ) <-> ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) )
209 208 anbi2d 
 |-  ( d = ( P ` 3 ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) <-> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) )
210 neeq2 
 |-  ( d = ( P ` 3 ) -> ( ( P ` 0 ) =/= d <-> ( P ` 0 ) =/= ( P ` 3 ) ) )
211 210 3anbi3d 
 |-  ( d = ( P ` 3 ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= d ) <-> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= ( P ` 3 ) ) ) )
212 neeq2 
 |-  ( d = ( P ` 3 ) -> ( ( P ` 1 ) =/= d <-> ( P ` 1 ) =/= ( P ` 3 ) ) )
213 neeq2 
 |-  ( d = ( P ` 3 ) -> ( ( P ` 2 ) =/= d <-> ( P ` 2 ) =/= ( P ` 3 ) ) )
214 212 213 3anbi23d 
 |-  ( d = ( P ` 3 ) -> ( ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= d /\ ( P ` 2 ) =/= d ) <-> ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 3 ) /\ ( P ` 2 ) =/= ( P ` 3 ) ) ) )
215 211 214 anbi12d 
 |-  ( d = ( P ` 3 ) -> ( ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= d /\ ( P ` 2 ) =/= d ) ) <-> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= ( P ` 3 ) ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 3 ) /\ ( P ` 2 ) =/= ( P ` 3 ) ) ) ) )
216 209 215 anbi12d 
 |-  ( d = ( P ` 3 ) -> ( ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= d /\ ( P ` 2 ) =/= d ) ) ) <-> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= ( P ` 3 ) ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 3 ) /\ ( P ` 2 ) =/= ( P ` 3 ) ) ) ) ) )
217 203 216 rspc2ev 
 |-  ( ( ( P ` 2 ) e. V /\ ( P ` 3 ) e. V /\ ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 0 ) =/= ( P ` 3 ) ) /\ ( ( P ` 1 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 3 ) /\ ( P ` 2 ) =/= ( P ` 3 ) ) ) ) ) -> E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) )
218 87 95 96 189 217 syl112anc 
 |-  ( ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) -> E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) )
219 71 79 218 3jca 
 |-  ( ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) ) -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) )
220 219 exp31 
 |-  ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) -> ( ( 4 e. NN0 /\ P : ( 0 ... 4 ) --> V ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) ) ) )
221 56 62 220 mp2and 
 |-  ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) ) )
222 221 adantr 
 |-  ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( P ` 0 ) = ( P ` 4 ) ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 0 ) } e. E ) ) -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) ) )
223 54 222 sylbid 
 |-  ( ( ( ( # ` F ) = 4 /\ F ( Paths ` G ) P ) /\ ( P ` 0 ) = ( P ` 4 ) ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) ) )
224 223 exp31 
 |-  ( ( # ` F ) = 4 -> ( F ( Paths ` G ) P -> ( ( P ` 0 ) = ( P ` 4 ) -> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) ) ) ) )
225 224 imp4c 
 |-  ( ( # ` F ) = 4 -> ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 4 ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) ) -> ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) ) )
226 preq1 
 |-  ( a = ( P ` 0 ) -> { a , b } = { ( P ` 0 ) , b } )
227 226 eleq1d 
 |-  ( a = ( P ` 0 ) -> ( { a , b } e. E <-> { ( P ` 0 ) , b } e. E ) )
228 227 anbi1d 
 |-  ( a = ( P ` 0 ) -> ( ( { a , b } e. E /\ { b , c } e. E ) <-> ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E ) ) )
229 preq2 
 |-  ( a = ( P ` 0 ) -> { d , a } = { d , ( P ` 0 ) } )
230 229 eleq1d 
 |-  ( a = ( P ` 0 ) -> ( { d , a } e. E <-> { d , ( P ` 0 ) } e. E ) )
231 230 anbi2d 
 |-  ( a = ( P ` 0 ) -> ( ( { c , d } e. E /\ { d , a } e. E ) <-> ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) )
232 228 231 anbi12d 
 |-  ( a = ( P ` 0 ) -> ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) <-> ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) ) )
233 neeq1 
 |-  ( a = ( P ` 0 ) -> ( a =/= b <-> ( P ` 0 ) =/= b ) )
234 neeq1 
 |-  ( a = ( P ` 0 ) -> ( a =/= c <-> ( P ` 0 ) =/= c ) )
235 neeq1 
 |-  ( a = ( P ` 0 ) -> ( a =/= d <-> ( P ` 0 ) =/= d ) )
236 233 234 235 3anbi123d 
 |-  ( a = ( P ` 0 ) -> ( ( a =/= b /\ a =/= c /\ a =/= d ) <-> ( ( P ` 0 ) =/= b /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) ) )
237 236 anbi1d 
 |-  ( a = ( P ` 0 ) -> ( ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) <-> ( ( ( P ` 0 ) =/= b /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) )
238 232 237 anbi12d 
 |-  ( a = ( P ` 0 ) -> ( ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) <-> ( ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= b /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) )
239 238 2rexbidv 
 |-  ( a = ( P ` 0 ) -> ( E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) <-> E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= b /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) )
240 preq2 
 |-  ( b = ( P ` 1 ) -> { ( P ` 0 ) , b } = { ( P ` 0 ) , ( P ` 1 ) } )
241 240 eleq1d 
 |-  ( b = ( P ` 1 ) -> ( { ( P ` 0 ) , b } e. E <-> { ( P ` 0 ) , ( P ` 1 ) } e. E ) )
242 preq1 
 |-  ( b = ( P ` 1 ) -> { b , c } = { ( P ` 1 ) , c } )
243 242 eleq1d 
 |-  ( b = ( P ` 1 ) -> ( { b , c } e. E <-> { ( P ` 1 ) , c } e. E ) )
244 241 243 anbi12d 
 |-  ( b = ( P ` 1 ) -> ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E ) <-> ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) ) )
245 244 anbi1d 
 |-  ( b = ( P ` 1 ) -> ( ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) <-> ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) ) )
246 neeq2 
 |-  ( b = ( P ` 1 ) -> ( ( P ` 0 ) =/= b <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
247 246 3anbi1d 
 |-  ( b = ( P ` 1 ) -> ( ( ( P ` 0 ) =/= b /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) <-> ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) ) )
248 neeq1 
 |-  ( b = ( P ` 1 ) -> ( b =/= c <-> ( P ` 1 ) =/= c ) )
249 neeq1 
 |-  ( b = ( P ` 1 ) -> ( b =/= d <-> ( P ` 1 ) =/= d ) )
250 248 249 3anbi12d 
 |-  ( b = ( P ` 1 ) -> ( ( b =/= c /\ b =/= d /\ c =/= d ) <-> ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) )
251 247 250 anbi12d 
 |-  ( b = ( P ` 1 ) -> ( ( ( ( P ` 0 ) =/= b /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) <-> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) )
252 245 251 anbi12d 
 |-  ( b = ( P ` 1 ) -> ( ( ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= b /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) <-> ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) )
253 252 2rexbidv 
 |-  ( b = ( P ` 1 ) -> ( E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= b /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) <-> E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) )
254 239 253 rspc2ev 
 |-  ( ( ( P ` 0 ) e. V /\ ( P ` 1 ) e. V /\ E. c e. V E. d e. V ( ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , c } e. E ) /\ ( { c , d } e. E /\ { d , ( P ` 0 ) } e. E ) ) /\ ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= c /\ ( P ` 0 ) =/= d ) /\ ( ( P ` 1 ) =/= c /\ ( P ` 1 ) =/= d /\ c =/= d ) ) ) ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) )
255 225 254 syl6 
 |-  ( ( # ` F ) = 4 -> ( ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` 4 ) ) /\ ( ( { ( P ` 0 ) , ( P ` 1 ) } e. E /\ { ( P ` 1 ) , ( P ` 2 ) } e. E ) /\ ( { ( P ` 2 ) , ( P ` 3 ) } e. E /\ { ( P ` 3 ) , ( P ` 4 ) } e. E ) ) ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) )
256 48 255 sylbid 
 |-  ( ( # ` F ) = 4 -> ( ( ( 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 E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) )
257 256 expd 
 |-  ( ( # ` F ) = 4 -> ( ( 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 E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) ) )
258 257 com13 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 4 -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) ) )
259 5 258 syl 
 |-  ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 4 -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) ) )
260 259 expcom 
 |-  ( F ( Walks ` G ) P -> ( G e. UPGraph -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 4 -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) ) ) )
261 260 com23 
 |-  ( F ( Walks ` G ) P -> ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( G e. UPGraph -> ( ( # ` F ) = 4 -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) ) ) )
262 261 expd 
 |-  ( F ( Walks ` G ) P -> ( F ( Paths ` G ) P -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( G e. UPGraph -> ( ( # ` F ) = 4 -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) ) ) ) )
263 4 262 mpcom 
 |-  ( F ( Paths ` G ) P -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( G e. UPGraph -> ( ( # ` F ) = 4 -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) ) ) )
264 263 imp 
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( G e. UPGraph -> ( ( # ` F ) = 4 -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) ) )
265 3 264 syl 
 |-  ( F ( Cycles ` G ) P -> ( G e. UPGraph -> ( ( # ` F ) = 4 -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) ) ) )
266 265 3imp21 
 |-  ( ( G e. UPGraph /\ F ( Cycles ` G ) P /\ ( # ` F ) = 4 ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( { a , b } e. E /\ { b , c } e. E ) /\ ( { c , d } e. E /\ { d , a } e. E ) ) /\ ( ( a =/= b /\ a =/= c /\ a =/= d ) /\ ( b =/= c /\ b =/= d /\ c =/= d ) ) ) )