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∧FCycles⁡GP∧F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈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 ⊢FCycles⁡GP→FPaths⁡GP∧P⁡0=P⁡F
4 pthiswlk ⊢FPaths⁡GP→FWalks⁡GP
5 2 upgrwlkvtxedg ⊢G∈UPGraph∧FWalks⁡GP→∀k∈0..^FP⁡kP⁡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→FPaths⁡GP∧P⁡0=P⁡F↔FPaths⁡GP∧P⁡0=P⁡4
9 oveq2 ⊢F=4→0..^F=0..^4
10 fzo0to42pr ⊢0..^4=01∪23
11 9 10 eqtrdi ⊢F=4→0..^F=01∪23
12 11 raleqdv ⊢F=4→∀k∈0..^FP⁡kP⁡k+1∈E↔∀k∈01∪23P⁡kP⁡k+1∈E
13 ralunb ⊢∀k∈01∪23P⁡kP⁡k+1∈E↔∀k∈01P⁡kP⁡k+1∈E∧∀k∈23P⁡kP⁡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⁡kP⁡k+1=P⁡0P⁡1
19 18 eleq1d ⊢k=0→P⁡kP⁡k+1∈E↔P⁡0P⁡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⁡kP⁡k+1=P⁡1P⁡2
26 25 eleq1d ⊢k=1→P⁡kP⁡k+1∈E↔P⁡1P⁡2∈E
27 14 15 19 26 ralpr ⊢∀k∈01P⁡kP⁡k+1∈E↔P⁡0P⁡1∈E∧P⁡1P⁡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⁡kP⁡k+1=P⁡2P⁡3
36 35 eleq1d ⊢k=2→P⁡kP⁡k+1∈E↔P⁡2P⁡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⁡kP⁡k+1=P⁡3P⁡4
43 42 eleq1d ⊢k=3→P⁡kP⁡k+1∈E↔P⁡3P⁡4∈E
44 28 29 36 43 ralpr ⊢∀k∈23P⁡kP⁡k+1∈E↔P⁡2P⁡3∈E∧P⁡3P⁡4∈E
45 27 44 anbi12i ⊢∀k∈01P⁡kP⁡k+1∈E∧∀k∈23P⁡kP⁡k+1∈E↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E
46 13 45 bitri ⊢∀k∈01∪23P⁡kP⁡k+1∈E↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E
47 12 46 bitrdi ⊢F=4→∀k∈0..^FP⁡kP⁡k+1∈E↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E
48 8 47 anbi12d ⊢F=4→FPaths⁡GP∧P⁡0=P⁡F∧∀k∈0..^FP⁡kP⁡k+1∈E↔FPaths⁡GP∧P⁡0=P⁡4∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E
49 preq2 ⊢P⁡4=P⁡0→P⁡3P⁡4=P⁡3P⁡0
50 49 eleq1d ⊢P⁡4=P⁡0→P⁡3P⁡4∈E↔P⁡3P⁡0∈E
51 50 eqcoms ⊢P⁡0=P⁡4→P⁡3P⁡4∈E↔P⁡3P⁡0∈E
52 51 anbi2d ⊢P⁡0=P⁡4→P⁡2P⁡3∈E∧P⁡3P⁡4∈E↔P⁡2P⁡3∈E∧P⁡3P⁡0∈E
53 52 anbi2d ⊢P⁡0=P⁡4→P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E
54 53 adantl ⊢F=4∧FPaths⁡GP∧P⁡0=P⁡4→P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E
55 4nn0 ⊢4∈ℕ0
56 55 a1i ⊢F=4∧FPaths⁡GP→4∈ℕ0
57 1 wlkp ⊢FWalks⁡GP→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 ⊢FPaths⁡GP→F=4→P:0…4⟶V
62 61 impcom ⊢F=4∧FPaths⁡GP→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∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡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∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡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∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡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∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E→P⁡3∈V
96 simpr ⊢F=4∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E→P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E
97 simplr ⊢F=4∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V→FPaths⁡GP
98 breq2 ⊢F=4→1<F↔1<4
99 74 98 mpbiri ⊢F=4→1<F
100 99 ad2antrr ⊢F=4∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V→1<F
101 simpll ⊢F=4∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V→F=4
102 9 ad2antrr ⊢F=4∧FPaths⁡GP∧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 ⊢FPaths⁡GP∧1<F∧0∈0..^F→P⁡0≠P⁡0+1
110 108 109 syl3an3 ⊢FPaths⁡GP∧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 ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→P⁡0≠P⁡1
115 simp1 ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→FPaths⁡GP
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 ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→2∈1..^F∧0∈0…F∧2≠0
130 pthdivtx ⊢FPaths⁡GP∧2∈1..^F∧0∈0…F∧2≠0→P⁡2≠P⁡0
131 115 129 130 syl2anc ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→P⁡2≠P⁡0
132 131 necomd ⊢FPaths⁡GP∧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 ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→3∈1..^F∧0∈0…F∧3≠0
143 pthdivtx ⊢FPaths⁡GP∧3∈1..^F∧0∈0…F∧3≠0→P⁡3≠P⁡0
144 115 142 143 syl2anc ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→P⁡3≠P⁡0
145 144 necomd ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→P⁡0≠P⁡3
146 114 132 145 3jca ⊢FPaths⁡GP∧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 ⊢FPaths⁡GP∧1<F∧1∈0..^F→P⁡1≠P⁡1+1
153 151 152 syl3an3 ⊢FPaths⁡GP∧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 ⊢FPaths⁡GP∧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 ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→1∈1..^F∧3∈0…F∧1≠3
175 pthdivtx ⊢FPaths⁡GP∧1∈1..^F∧3∈0…F∧1≠3→P⁡1≠P⁡3
176 115 174 175 syl2anc ⊢FPaths⁡GP∧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 ⊢FPaths⁡GP∧1<F∧2∈0..^F→P⁡2≠P⁡2+1
181 179 180 syl3an3 ⊢FPaths⁡GP∧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 ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→P⁡2≠P⁡3
186 157 176 185 3jca ⊢FPaths⁡GP∧1<F∧F=4∧0..^F=0..^4→P⁡1≠P⁡2∧P⁡1≠P⁡3∧P⁡2≠P⁡3
187 146 186 jca ⊢FPaths⁡GP∧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∧FPaths⁡GP∧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∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡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⁡1c=P⁡1P⁡2
191 190 eleq1d ⊢c=P⁡2→P⁡1c∈E↔P⁡1P⁡2∈E
192 191 anbi2d ⊢c=P⁡2→P⁡0P⁡1∈E∧P⁡1c∈E↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E
193 preq1 ⊢c=P⁡2→cd=P⁡2d
194 193 eleq1d ⊢c=P⁡2→cd∈E↔P⁡2d∈E
195 194 anbi1d ⊢c=P⁡2→cd∈E∧dP⁡0∈E↔P⁡2d∈E∧dP⁡0∈E
196 192 195 anbi12d ⊢c=P⁡2→P⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡0∈E↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2d∈E∧dP⁡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⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡0∈E∧P⁡0≠P⁡1∧P⁡0≠c∧P⁡0≠d∧P⁡1≠c∧P⁡1≠d∧c≠d↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2d∈E∧dP⁡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⁡2d=P⁡2P⁡3
205 204 eleq1d ⊢d=P⁡3→P⁡2d∈E↔P⁡2P⁡3∈E
206 preq1 ⊢d=P⁡3→dP⁡0=P⁡3P⁡0
207 206 eleq1d ⊢d=P⁡3→dP⁡0∈E↔P⁡3P⁡0∈E
208 205 207 anbi12d ⊢d=P⁡3→P⁡2d∈E∧dP⁡0∈E↔P⁡2P⁡3∈E∧P⁡3P⁡0∈E
209 208 anbi2d ⊢d=P⁡3→P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2d∈E∧dP⁡0∈E↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡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⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2d∈E∧dP⁡0∈E∧P⁡0≠P⁡1∧P⁡0≠P⁡2∧P⁡0≠d∧P⁡1≠P⁡2∧P⁡1≠d∧P⁡2≠d↔P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡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⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡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∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E→∃c∈V∃d∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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∧FPaths⁡GP∧4∈ℕ0∧P:0…4⟶V∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E→P⁡0∈V∧P⁡1∈V∧∃c∈V∃d∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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∧FPaths⁡GP→4∈ℕ0∧P:0…4⟶V→P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E→P⁡0∈V∧P⁡1∈V∧∃c∈V∃d∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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∧FPaths⁡GP→P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E→P⁡0∈V∧P⁡1∈V∧∃c∈V∃d∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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∧FPaths⁡GP∧P⁡0=P⁡4→P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡0∈E→P⁡0∈V∧P⁡1∈V∧∃c∈V∃d∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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∧FPaths⁡GP∧P⁡0=P⁡4→P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E→P⁡0∈V∧P⁡1∈V∧∃c∈V∃d∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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→FPaths⁡GP→P⁡0=P⁡4→P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E→P⁡0∈V∧P⁡1∈V∧∃c∈V∃d∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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→FPaths⁡GP∧P⁡0=P⁡4∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E→P⁡0∈V∧P⁡1∈V∧∃c∈V∃d∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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→ab=P⁡0b
227 226 eleq1d ⊢a=P⁡0→ab∈E↔P⁡0b∈E
228 227 anbi1d ⊢a=P⁡0→ab∈E∧bc∈E↔P⁡0b∈E∧bc∈E
229 preq2 ⊢a=P⁡0→da=dP⁡0
230 229 eleq1d ⊢a=P⁡0→da∈E↔dP⁡0∈E
231 230 anbi2d ⊢a=P⁡0→cd∈E∧da∈E↔cd∈E∧dP⁡0∈E
232 228 231 anbi12d ⊢a=P⁡0→ab∈E∧bc∈E∧cd∈E∧da∈E↔P⁡0b∈E∧bc∈E∧cd∈E∧dP⁡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→ab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d↔P⁡0b∈E∧bc∈E∧cd∈E∧dP⁡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∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d↔∃c∈V∃d∈VP⁡0b∈E∧bc∈E∧cd∈E∧dP⁡0∈E∧P⁡0≠b∧P⁡0≠c∧P⁡0≠d∧b≠c∧b≠d∧c≠d
240 preq2 ⊢b=P⁡1→P⁡0b=P⁡0P⁡1
241 240 eleq1d ⊢b=P⁡1→P⁡0b∈E↔P⁡0P⁡1∈E
242 preq1 ⊢b=P⁡1→bc=P⁡1c
243 242 eleq1d ⊢b=P⁡1→bc∈E↔P⁡1c∈E
244 241 243 anbi12d ⊢b=P⁡1→P⁡0b∈E∧bc∈E↔P⁡0P⁡1∈E∧P⁡1c∈E
245 244 anbi1d ⊢b=P⁡1→P⁡0b∈E∧bc∈E∧cd∈E∧dP⁡0∈E↔P⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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⁡0b∈E∧bc∈E∧cd∈E∧dP⁡0∈E∧P⁡0≠b∧P⁡0≠c∧P⁡0≠d∧b≠c∧b≠d∧c≠d↔P⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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∈VP⁡0b∈E∧bc∈E∧cd∈E∧dP⁡0∈E∧P⁡0≠b∧P⁡0≠c∧P⁡0≠d∧b≠c∧b≠d∧c≠d↔∃c∈V∃d∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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∈VP⁡0P⁡1∈E∧P⁡1c∈E∧cd∈E∧dP⁡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∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
255 225 254 syl6 ⊢F=4→FPaths⁡GP∧P⁡0=P⁡4∧P⁡0P⁡1∈E∧P⁡1P⁡2∈E∧P⁡2P⁡3∈E∧P⁡3P⁡4∈E→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
256 48 255 sylbid ⊢F=4→FPaths⁡GP∧P⁡0=P⁡F∧∀k∈0..^FP⁡kP⁡k+1∈E→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
257 256 expd ⊢F=4→FPaths⁡GP∧P⁡0=P⁡F→∀k∈0..^FP⁡kP⁡k+1∈E→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
258 257 com13 ⊢∀k∈0..^FP⁡kP⁡k+1∈E→FPaths⁡GP∧P⁡0=P⁡F→F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
259 5 258 syl ⊢G∈UPGraph∧FWalks⁡GP→FPaths⁡GP∧P⁡0=P⁡F→F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
260 259 expcom ⊢FWalks⁡GP→G∈UPGraph→FPaths⁡GP∧P⁡0=P⁡F→F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
261 260 com23 ⊢FWalks⁡GP→FPaths⁡GP∧P⁡0=P⁡F→G∈UPGraph→F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
262 261 expd ⊢FWalks⁡GP→FPaths⁡GP→P⁡0=P⁡F→G∈UPGraph→F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
263 4 262 mpcom ⊢FPaths⁡GP→P⁡0=P⁡F→G∈UPGraph→F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
264 263 imp ⊢FPaths⁡GP∧P⁡0=P⁡F→G∈UPGraph→F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
265 3 264 syl ⊢FCycles⁡GP→G∈UPGraph→F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d
266 265 3imp21 ⊢G∈UPGraph∧FCycles⁡GP∧F=4→∃a∈V∃b∈V∃c∈V∃d∈Vab∈E∧bc∈E∧cd∈E∧da∈E∧a≠b∧a≠c∧a≠d∧b≠c∧b≠d∧c≠d