Step | Hyp | Ref
| Expression |
1 | | konigsberg.v |
. . 3
β’ π = (0...3) |
2 | | konigsberg.e |
. . 3
β’ πΈ = β¨β{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© |
3 | | konigsberg.g |
. . 3
β’ πΊ = β¨π, πΈβ© |
4 | 1, 2, 3 | konigsberglem4 29202 |
. 2
β’ {0, 1, 3}
β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} |
5 | 1 | ovexi 7392 |
. . . 4
β’ π β V |
6 | 5 | rabex 5290 |
. . 3
β’ {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β V |
7 | | hashss 14310 |
. . 3
β’ (({π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β V β§ {0, 1, 3} β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β (β―β{0, 1, 3}) β€
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
8 | 6, 7 | mpan 689 |
. 2
β’ ({0, 1,
3} β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β (β―β{0, 1, 3}) β€
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
9 | | 0ne1 12225 |
. . . . . 6
β’ 0 β
1 |
10 | | 1re 11156 |
. . . . . . 7
β’ 1 β
β |
11 | | 1lt3 12327 |
. . . . . . 7
β’ 1 <
3 |
12 | 10, 11 | ltneii 11269 |
. . . . . 6
β’ 1 β
3 |
13 | | 3ne0 12260 |
. . . . . 6
β’ 3 β
0 |
14 | 9, 12, 13 | 3pm3.2i 1340 |
. . . . 5
β’ (0 β 1
β§ 1 β 3 β§ 3 β 0) |
15 | | c0ex 11150 |
. . . . . 6
β’ 0 β
V |
16 | | 1ex 11152 |
. . . . . 6
β’ 1 β
V |
17 | | 3ex 12236 |
. . . . . 6
β’ 3 β
V |
18 | | hashtpg 14385 |
. . . . . 6
β’ ((0
β V β§ 1 β V β§ 3 β V) β ((0 β 1 β§ 1 β 3
β§ 3 β 0) β (β―β{0, 1, 3}) = 3)) |
19 | 15, 16, 17, 18 | mp3an 1462 |
. . . . 5
β’ ((0 β
1 β§ 1 β 3 β§ 3 β 0) β (β―β{0, 1, 3}) =
3) |
20 | 14, 19 | mpbi 229 |
. . . 4
β’
(β―β{0, 1, 3}) = 3 |
21 | 20 | breq1i 5113 |
. . 3
β’
((β―β{0, 1, 3}) β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β 3 β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
22 | | df-3 12218 |
. . . . 5
β’ 3 = (2 +
1) |
23 | 22 | breq1i 5113 |
. . . 4
β’ (3 β€
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β (2 + 1) β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
24 | | 2z 12536 |
. . . . 5
β’ 2 β
β€ |
25 | | fzfi 13878 |
. . . . . . . 8
β’ (0...3)
β Fin |
26 | 1, 25 | eqeltri 2834 |
. . . . . . 7
β’ π β Fin |
27 | | rabfi 9214 |
. . . . . . 7
β’ (π β Fin β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β Fin) |
28 | | hashcl 14257 |
. . . . . . 7
β’ ({π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β Fin β (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β
β0) |
29 | 26, 27, 28 | mp2b 10 |
. . . . . 6
β’
(β―β{π₯
β π β£ Β¬ 2
β₯ ((VtxDegβπΊ)βπ₯)}) β
β0 |
30 | 29 | nn0zi 12529 |
. . . . 5
β’
(β―β{π₯
β π β£ Β¬ 2
β₯ ((VtxDegβπΊ)βπ₯)}) β β€ |
31 | | zltp1le 12554 |
. . . . 5
β’ ((2
β β€ β§ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β β€) β (2 <
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β (2 + 1) β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}))) |
32 | 24, 30, 31 | mp2an 691 |
. . . 4
β’ (2 <
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β (2 + 1) β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
33 | 23, 32 | sylbb2 237 |
. . 3
β’ (3 β€
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β 2 < (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
34 | 21, 33 | sylbi 216 |
. 2
β’
((β―β{0, 1, 3}) β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β 2 < (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
35 | 4, 8, 34 | mp2b 10 |
1
β’ 2 <
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) |