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 ∈ UPGraph ∧ F Cycles ⁡ G P ∧ F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ 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 ∈ UPGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ 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 ∪ 2 3
11 9 10 eqtrdi ⊢ F = 4 → 0 ..^ F = 0 1 ∪ 2 3
12 11 raleqdv ⊢ F = 4 → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E ↔ ∀ k ∈ 0 1 ∪ 2 3 P ⁡ k P ⁡ k + 1 ∈ E
13 ralunb ⊢ ∀ k ∈ 0 1 ∪ 2 3 P ⁡ k P ⁡ k + 1 ∈ E ↔ ∀ k ∈ 0 1 P ⁡ k P ⁡ k + 1 ∈ E ∧ ∀ k ∈ 2 3 P ⁡ k P ⁡ k + 1 ∈ E
14 c0ex ⊢ 0 ∈ V
15 1ex ⊢ 1 ∈ 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 ↔ P ⁡ 0 P ⁡ 1 ∈ 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 ↔ P ⁡ 1 P ⁡ 2 ∈ E
27 14 15 19 26 ralpr ⊢ ∀ k ∈ 0 1 P ⁡ k P ⁡ k + 1 ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E
28 2ex ⊢ 2 ∈ V
29 3ex ⊢ 3 ∈ 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 ↔ P ⁡ 2 P ⁡ 3 ∈ 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 ↔ P ⁡ 3 P ⁡ 4 ∈ E
44 28 29 36 43 ralpr ⊢ ∀ k ∈ 2 3 P ⁡ k P ⁡ k + 1 ∈ E ↔ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E
45 27 44 anbi12i ⊢ ∀ k ∈ 0 1 P ⁡ k P ⁡ k + 1 ∈ E ∧ ∀ k ∈ 2 3 P ⁡ k P ⁡ k + 1 ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E
46 13 45 bitri ⊢ ∀ k ∈ 0 1 ∪ 2 3 P ⁡ k P ⁡ k + 1 ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E
47 12 46 bitrdi ⊢ F = 4 → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E
48 8 47 anbi12d ⊢ F = 4 → F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F ∧ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E ↔ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ 4 ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ 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 ↔ P ⁡ 3 P ⁡ 0 ∈ E
51 50 eqcoms ⊢ P ⁡ 0 = P ⁡ 4 → P ⁡ 3 P ⁡ 4 ∈ E ↔ P ⁡ 3 P ⁡ 0 ∈ E
52 51 anbi2d ⊢ P ⁡ 0 = P ⁡ 4 → P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E ↔ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E
53 52 anbi2d ⊢ P ⁡ 0 = P ⁡ 4 → P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E
54 53 adantl ⊢ F = 4 ∧ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ 4 → P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E
55 4nn0 ⊢ 4 ∈ ℕ 0
56 55 a1i ⊢ F = 4 ∧ F Paths ⁡ G P → 4 ∈ ℕ 0
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 ∈ ℕ 0 → 4 ∈ ℕ 0
64 0nn0 ⊢ 0 ∈ ℕ 0
65 64 a1i ⊢ 4 ∈ ℕ 0 → 0 ∈ ℕ 0
66 4pos ⊢ 0 < 4
67 66 a1i ⊢ 4 ∈ ℕ 0 → 0 < 4
68 63 65 67 3jca ⊢ 4 ∈ ℕ 0 → 4 ∈ ℕ 0 ∧ 0 ∈ ℕ 0 ∧ 0 < 4
69 fvffz0 ⊢ 4 ∈ ℕ 0 ∧ 0 ∈ ℕ 0 ∧ 0 < 4 ∧ P : 0 … 4 ⟶ V → P ⁡ 0 ∈ V
70 68 69 sylan ⊢ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V → P ⁡ 0 ∈ V
71 70 ad2antlr ⊢ F = 4 ∧ F Paths ⁡ G P ∧ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → P ⁡ 0 ∈ V
72 1nn0 ⊢ 1 ∈ ℕ 0
73 72 a1i ⊢ 4 ∈ ℕ 0 → 1 ∈ ℕ 0
74 1lt4 ⊢ 1 < 4
75 74 a1i ⊢ 4 ∈ ℕ 0 → 1 < 4
76 63 73 75 3jca ⊢ 4 ∈ ℕ 0 → 4 ∈ ℕ 0 ∧ 1 ∈ ℕ 0 ∧ 1 < 4
77 fvffz0 ⊢ 4 ∈ ℕ 0 ∧ 1 ∈ ℕ 0 ∧ 1 < 4 ∧ P : 0 … 4 ⟶ V → P ⁡ 1 ∈ V
78 76 77 sylan ⊢ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V → P ⁡ 1 ∈ V
79 78 ad2antlr ⊢ F = 4 ∧ F Paths ⁡ G P ∧ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → P ⁡ 1 ∈ V
80 2nn0 ⊢ 2 ∈ ℕ 0
81 80 a1i ⊢ 4 ∈ ℕ 0 → 2 ∈ ℕ 0
82 2lt4 ⊢ 2 < 4
83 82 a1i ⊢ 4 ∈ ℕ 0 → 2 < 4
84 63 81 83 3jca ⊢ 4 ∈ ℕ 0 → 4 ∈ ℕ 0 ∧ 2 ∈ ℕ 0 ∧ 2 < 4
85 fvffz0 ⊢ 4 ∈ ℕ 0 ∧ 2 ∈ ℕ 0 ∧ 2 < 4 ∧ P : 0 … 4 ⟶ V → P ⁡ 2 ∈ V
86 84 85 sylan ⊢ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V → P ⁡ 2 ∈ V
87 86 ad2antlr ⊢ F = 4 ∧ F Paths ⁡ G P ∧ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → P ⁡ 2 ∈ V
88 3nn0 ⊢ 3 ∈ ℕ 0
89 88 a1i ⊢ 4 ∈ ℕ 0 → 3 ∈ ℕ 0
90 3lt4 ⊢ 3 < 4
91 90 a1i ⊢ 4 ∈ ℕ 0 → 3 < 4
92 63 89 91 3jca ⊢ 4 ∈ ℕ 0 → 4 ∈ ℕ 0 ∧ 3 ∈ ℕ 0 ∧ 3 < 4
93 fvffz0 ⊢ 4 ∈ ℕ 0 ∧ 3 ∈ ℕ 0 ∧ 3 < 4 ∧ P : 0 … 4 ⟶ V → P ⁡ 3 ∈ V
94 92 93 sylan ⊢ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V → P ⁡ 3 ∈ V
95 94 ad2antlr ⊢ F = 4 ∧ F Paths ⁡ G P ∧ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → P ⁡ 3 ∈ V
96 simpr ⊢ F = 4 ∧ F Paths ⁡ G P ∧ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E
97 simplr ⊢ F = 4 ∧ F Paths ⁡ G P ∧ 4 ∈ ℕ 0 ∧ 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 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V → 1 < F
101 simpll ⊢ F = 4 ∧ F Paths ⁡ G P ∧ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V → F = 4
102 9 ad2antrr ⊢ F = 4 ∧ F Paths ⁡ G P ∧ 4 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V → 0 ..^ F = 0 ..^ 4
103 4nn ⊢ 4 ∈ ℕ
104 lbfzo0 ⊢ 0 ∈ 0 ..^ 4 ↔ 4 ∈ ℕ
105 103 104 mpbir ⊢ 0 ∈ 0 ..^ 4
106 eleq2 ⊢ 0 ..^ F = 0 ..^ 4 → 0 ∈ 0 ..^ F ↔ 0 ∈ 0 ..^ 4
107 105 106 mpbiri ⊢ 0 ..^ F = 0 ..^ 4 → 0 ∈ 0 ..^ F
108 107 adantl ⊢ F = 4 ∧ 0 ..^ F = 0 ..^ 4 → 0 ∈ 0 ..^ F
109 pthdadjvtx ⊢ F Paths ⁡ G P ∧ 1 < F ∧ 0 ∈ 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 ∈ 0 ..^ 4 ↔ 2 ∈ ℕ 0 ∧ 4 ∈ ℕ ∧ 2 < 4
117 80 103 82 116 mpbir3an ⊢ 2 ∈ 0 ..^ 4
118 2ne0 ⊢ 2 ≠ 0
119 fzo1fzo0n0 ⊢ 2 ∈ 1 ..^ 4 ↔ 2 ∈ 0 ..^ 4 ∧ 2 ≠ 0
120 117 118 119 mpbir2an ⊢ 2 ∈ 1 ..^ 4
121 oveq2 ⊢ F = 4 → 1 ..^ F = 1 ..^ 4
122 120 121 eleqtrrid ⊢ F = 4 → 2 ∈ 1 ..^ F
123 0elfz ⊢ 4 ∈ ℕ 0 → 0 ∈ 0 … 4
124 55 123 ax-mp ⊢ 0 ∈ 0 … 4
125 124 58 eleqtrrid ⊢ F = 4 → 0 ∈ 0 … F
126 118 a1i ⊢ F = 4 → 2 ≠ 0
127 122 125 126 3jca ⊢ F = 4 → 2 ∈ 1 ..^ F ∧ 0 ∈ 0 … F ∧ 2 ≠ 0
128 127 adantr ⊢ F = 4 ∧ 0 ..^ F = 0 ..^ 4 → 2 ∈ 1 ..^ F ∧ 0 ∈ 0 … F ∧ 2 ≠ 0
129 128 3ad2ant3 ⊢ F Paths ⁡ G P ∧ 1 < F ∧ F = 4 ∧ 0 ..^ F = 0 ..^ 4 → 2 ∈ 1 ..^ F ∧ 0 ∈ 0 … F ∧ 2 ≠ 0
130 pthdivtx ⊢ F Paths ⁡ G P ∧ 2 ∈ 1 ..^ F ∧ 0 ∈ 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 ∈ 0 ..^ 4 ↔ 3 ∈ ℕ 0 ∧ 4 ∈ ℕ ∧ 3 < 4
134 88 103 90 133 mpbir3an ⊢ 3 ∈ 0 ..^ 4
135 3ne0 ⊢ 3 ≠ 0
136 fzo1fzo0n0 ⊢ 3 ∈ 1 ..^ 4 ↔ 3 ∈ 0 ..^ 4 ∧ 3 ≠ 0
137 134 135 136 mpbir2an ⊢ 3 ∈ 1 ..^ 4
138 137 121 eleqtrrid ⊢ F = 4 → 3 ∈ 1 ..^ F
139 135 a1i ⊢ F = 4 → 3 ≠ 0
140 138 125 139 3jca ⊢ F = 4 → 3 ∈ 1 ..^ F ∧ 0 ∈ 0 … F ∧ 3 ≠ 0
141 140 adantr ⊢ F = 4 ∧ 0 ..^ F = 0 ..^ 4 → 3 ∈ 1 ..^ F ∧ 0 ∈ 0 … F ∧ 3 ≠ 0
142 141 3ad2ant3 ⊢ F Paths ⁡ G P ∧ 1 < F ∧ F = 4 ∧ 0 ..^ F = 0 ..^ 4 → 3 ∈ 1 ..^ F ∧ 0 ∈ 0 … F ∧ 3 ≠ 0
143 pthdivtx ⊢ F Paths ⁡ G P ∧ 3 ∈ 1 ..^ F ∧ 0 ∈ 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 ∈ 0 ..^ 4 ↔ 1 ∈ ℕ 0 ∧ 4 ∈ ℕ ∧ 1 < 4
148 72 103 74 147 mpbir3an ⊢ 1 ∈ 0 ..^ 4
149 eleq2 ⊢ 0 ..^ F = 0 ..^ 4 → 1 ∈ 0 ..^ F ↔ 1 ∈ 0 ..^ 4
150 148 149 mpbiri ⊢ 0 ..^ F = 0 ..^ 4 → 1 ∈ 0 ..^ F
151 150 adantl ⊢ F = 4 ∧ 0 ..^ F = 0 ..^ 4 → 1 ∈ 0 ..^ F
152 pthdadjvtx ⊢ F Paths ⁡ G P ∧ 1 < F ∧ 1 ∈ 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 ∈ 1 ..^ 4 ↔ 1 ∈ 0 ..^ 4 ∧ 1 ≠ 0
160 148 158 159 mpbir2an ⊢ 1 ∈ 1 ..^ 4
161 160 121 eleqtrrid ⊢ F = 4 → 1 ∈ 1 ..^ F
162 3re ⊢ 3 ∈ ℝ
163 4re ⊢ 4 ∈ ℝ
164 162 163 90 ltleii ⊢ 3 ≤ 4
165 elfz2nn0 ⊢ 3 ∈ 0 … 4 ↔ 3 ∈ ℕ 0 ∧ 4 ∈ ℕ 0 ∧ 3 ≤ 4
166 88 55 164 165 mpbir3an ⊢ 3 ∈ 0 … 4
167 166 58 eleqtrrid ⊢ F = 4 → 3 ∈ 0 … F
168 1re ⊢ 1 ∈ ℝ
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 ∈ 1 ..^ F ∧ 3 ∈ 0 … F ∧ 1 ≠ 3
173 172 adantr ⊢ F = 4 ∧ 0 ..^ F = 0 ..^ 4 → 1 ∈ 1 ..^ F ∧ 3 ∈ 0 … F ∧ 1 ≠ 3
174 173 3ad2ant3 ⊢ F Paths ⁡ G P ∧ 1 < F ∧ F = 4 ∧ 0 ..^ F = 0 ..^ 4 → 1 ∈ 1 ..^ F ∧ 3 ∈ 0 … F ∧ 1 ≠ 3
175 pthdivtx ⊢ F Paths ⁡ G P ∧ 1 ∈ 1 ..^ F ∧ 3 ∈ 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 ∈ 0 ..^ F ↔ 2 ∈ 0 ..^ 4
178 117 177 mpbiri ⊢ 0 ..^ F = 0 ..^ 4 → 2 ∈ 0 ..^ F
179 178 adantl ⊢ F = 4 ∧ 0 ..^ F = 0 ..^ 4 → 2 ∈ 0 ..^ F
180 pthdadjvtx ⊢ F Paths ⁡ G P ∧ 1 < F ∧ 2 ∈ 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 ∈ ℕ 0 ∧ 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 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ 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 ↔ P ⁡ 1 P ⁡ 2 ∈ E
192 191 anbi2d ⊢ c = P ⁡ 2 → P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E
193 preq1 ⊢ c = P ⁡ 2 → c d = P ⁡ 2 d
194 193 eleq1d ⊢ c = P ⁡ 2 → c d ∈ E ↔ P ⁡ 2 d ∈ E
195 194 anbi1d ⊢ c = P ⁡ 2 → c d ∈ E ∧ d P ⁡ 0 ∈ E ↔ P ⁡ 2 d ∈ E ∧ d P ⁡ 0 ∈ E
196 192 195 anbi12d ⊢ c = P ⁡ 2 → P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 d ∈ E ∧ d P ⁡ 0 ∈ 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 ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ E ∧ P ⁡ 0 ≠ P ⁡ 1 ∧ P ⁡ 0 ≠ c ∧ P ⁡ 0 ≠ d ∧ P ⁡ 1 ≠ c ∧ P ⁡ 1 ≠ d ∧ c ≠ d ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 d ∈ E ∧ d P ⁡ 0 ∈ 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 ↔ P ⁡ 2 P ⁡ 3 ∈ E
206 preq1 ⊢ d = P ⁡ 3 → d P ⁡ 0 = P ⁡ 3 P ⁡ 0
207 206 eleq1d ⊢ d = P ⁡ 3 → d P ⁡ 0 ∈ E ↔ P ⁡ 3 P ⁡ 0 ∈ E
208 205 207 anbi12d ⊢ d = P ⁡ 3 → P ⁡ 2 d ∈ E ∧ d P ⁡ 0 ∈ E ↔ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E
209 208 anbi2d ⊢ d = P ⁡ 3 → P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 d ∈ E ∧ d P ⁡ 0 ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ 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 ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 d ∈ E ∧ d P ⁡ 0 ∈ 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 ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ 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 ∈ V ∧ P ⁡ 3 ∈ V ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ 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 → ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V ∧ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∈ ℕ 0 ∧ P : 0 … 4 ⟶ V → P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 0 ∈ E → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E → P ⁡ 0 ∈ V ∧ P ⁡ 1 ∈ V ∧ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ↔ P ⁡ 0 b ∈ E
228 227 anbi1d ⊢ a = P ⁡ 0 → a b ∈ E ∧ b c ∈ E ↔ P ⁡ 0 b ∈ E ∧ b c ∈ E
229 preq2 ⊢ a = P ⁡ 0 → d a = d P ⁡ 0
230 229 eleq1d ⊢ a = P ⁡ 0 → d a ∈ E ↔ d P ⁡ 0 ∈ E
231 230 anbi2d ⊢ a = P ⁡ 0 → c d ∈ E ∧ d a ∈ E ↔ c d ∈ E ∧ d P ⁡ 0 ∈ E
232 228 231 anbi12d ⊢ a = P ⁡ 0 → a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ E ↔ P ⁡ 0 b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ E ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ↔ P ⁡ 0 b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ E ∧ P ⁡ 0 ≠ b ∧ P ⁡ 0 ≠ c ∧ P ⁡ 0 ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
239 238 2rexbidv ⊢ a = P ⁡ 0 → ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ E ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ↔ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ↔ P ⁡ 0 P ⁡ 1 ∈ E
242 preq1 ⊢ b = P ⁡ 1 → b c = P ⁡ 1 c
243 242 eleq1d ⊢ b = P ⁡ 1 → b c ∈ E ↔ P ⁡ 1 c ∈ E
244 241 243 anbi12d ⊢ b = P ⁡ 1 → P ⁡ 0 b ∈ E ∧ b c ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E
245 244 anbi1d ⊢ b = P ⁡ 1 → P ⁡ 0 b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ E ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∧ b c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ E ∧ P ⁡ 0 ≠ b ∧ P ⁡ 0 ≠ c ∧ P ⁡ 0 ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ↔ P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 → ∃ c ∈ V ∃ d ∈ V P ⁡ 0 b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ E ∧ P ⁡ 0 ≠ b ∧ P ⁡ 0 ≠ c ∧ P ⁡ 0 ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ↔ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ 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 ∈ V ∧ P ⁡ 1 ∈ V ∧ ∃ c ∈ V ∃ d ∈ V P ⁡ 0 P ⁡ 1 ∈ E ∧ P ⁡ 1 c ∈ E ∧ c d ∈ E ∧ d P ⁡ 0 ∈ E ∧ P ⁡ 0 ≠ P ⁡ 1 ∧ P ⁡ 0 ≠ c ∧ P ⁡ 0 ≠ d ∧ P ⁡ 1 ≠ c ∧ P ⁡ 1 ≠ d ∧ c ≠ d → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ 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 ∧ P ⁡ 1 P ⁡ 2 ∈ E ∧ P ⁡ 2 P ⁡ 3 ∈ E ∧ P ⁡ 3 P ⁡ 4 ∈ E → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ 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 ∧ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ 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 → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ E ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
258 257 com13 ⊢ ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E → F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F → F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ E ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
259 5 258 syl ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P → F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F → F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ E ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
260 259 expcom ⊢ F Walks ⁡ G P → G ∈ UPGraph → F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F → F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ 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 ∈ UPGraph → F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ 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 ∈ UPGraph → F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ 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 ∈ UPGraph → F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ 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 ∈ UPGraph → F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ E ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
265 3 264 syl ⊢ F Cycles ⁡ G P → G ∈ UPGraph → F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ E ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
266 265 3imp21 ⊢ G ∈ UPGraph ∧ F Cycles ⁡ G P ∧ F = 4 → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V ∃ d ∈ V a b ∈ E ∧ b c ∈ E ∧ c d ∈ E ∧ d a ∈ E ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d