| 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 30121 |
. 2
β’ {0, 1, 3}
β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} |
| 5 | 1 | ovexi 7451 |
. . . 4
β’ π β V |
| 6 | 5 | rabex 5334 |
. . 3
β’ {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β V |
| 7 | | hashss 14400 |
. . 3
β’ (({π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β V β§ {0, 1, 3} β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β (β―β{0, 1, 3}) β€
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
| 8 | 6, 7 | mpan 688 |
. 2
β’ ({0, 1,
3} β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β (β―β{0, 1, 3}) β€
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
| 9 | | 0ne1 12313 |
. . . . . 6
β’ 0 β
1 |
| 10 | | 1re 11244 |
. . . . . . 7
β’ 1 β
β |
| 11 | | 1lt3 12415 |
. . . . . . 7
β’ 1 <
3 |
| 12 | 10, 11 | ltneii 11357 |
. . . . . 6
β’ 1 β
3 |
| 13 | | 3ne0 12348 |
. . . . . 6
β’ 3 β
0 |
| 14 | 9, 12, 13 | 3pm3.2i 1336 |
. . . . 5
β’ (0 β 1
β§ 1 β 3 β§ 3 β 0) |
| 15 | | c0ex 11238 |
. . . . . 6
β’ 0 β
V |
| 16 | | 1ex 11240 |
. . . . . 6
β’ 1 β
V |
| 17 | | 3ex 12324 |
. . . . . 6
β’ 3 β
V |
| 18 | | hashtpg 14478 |
. . . . . 6
β’ ((0
β V β§ 1 β V β§ 3 β V) β ((0 β 1 β§ 1 β 3
β§ 3 β 0) β (β―β{0, 1, 3}) = 3)) |
| 19 | 15, 16, 17, 18 | mp3an 1457 |
. . . . 5
β’ ((0 β
1 β§ 1 β 3 β§ 3 β 0) β (β―β{0, 1, 3}) =
3) |
| 20 | 14, 19 | mpbi 229 |
. . . 4
β’
(β―β{0, 1, 3}) = 3 |
| 21 | 20 | breq1i 5155 |
. . 3
β’
((β―β{0, 1, 3}) β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β 3 β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
| 22 | | df-3 12306 |
. . . . 5
β’ 3 = (2 +
1) |
| 23 | 22 | breq1i 5155 |
. . . 4
β’ (3 β€
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β (2 + 1) β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)})) |
| 24 | | 2z 12624 |
. . . . 5
β’ 2 β
β€ |
| 25 | | fzfi 13969 |
. . . . . . . 8
β’ (0...3)
β Fin |
| 26 | 1, 25 | eqeltri 2821 |
. . . . . . 7
β’ π β Fin |
| 27 | | rabfi 9292 |
. . . . . . 7
β’ (π β Fin β {π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β Fin) |
| 28 | | hashcl 14347 |
. . . . . . 7
β’ ({π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)} β Fin β (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β
β0) |
| 29 | 26, 27, 28 | mp2b 10 |
. . . . . 6
β’
(β―β{π₯
β π β£ Β¬ 2
β₯ ((VtxDegβπΊ)βπ₯)}) β
β0 |
| 30 | 29 | nn0zi 12617 |
. . . . 5
β’
(β―β{π₯
β π β£ Β¬ 2
β₯ ((VtxDegβπΊ)βπ₯)}) β β€ |
| 31 | | zltp1le 12642 |
. . . . 5
β’ ((2
β β€ β§ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β β€) β (2 <
(β―β{π₯ β
π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}) β (2 + 1) β€ (β―β{π₯ β π β£ Β¬ 2 β₯
((VtxDegβπΊ)βπ₯)}))) |
| 32 | 24, 30, 31 | mp2an 690 |
. . . 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βπΊ)βπ₯)}) |
