Step |
Hyp |
Ref |
Expression |
1 |
|
konigsberg.v |
β’ π = ( 0 ... 3 ) |
2 |
|
konigsberg.e |
β’ πΈ = β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© |
3 |
|
konigsberg.g |
β’ πΊ = β¨ π , πΈ β© |
4 |
1 2 3
|
konigsberglem4 |
β’ { 0 , 1 , 3 } β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } |
5 |
1
|
ovexi |
β’ π β V |
6 |
5
|
rabex |
β’ { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } β V |
7 |
|
hashss |
β’ ( ( { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } β V β§ { 0 , 1 , 3 } β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β ( β― β { 0 , 1 , 3 } ) β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) ) |
8 |
6 7
|
mpan |
β’ ( { 0 , 1 , 3 } β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } β ( β― β { 0 , 1 , 3 } ) β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) ) |
9 |
|
0ne1 |
β’ 0 β 1 |
10 |
|
1re |
β’ 1 β β |
11 |
|
1lt3 |
β’ 1 < 3 |
12 |
10 11
|
ltneii |
β’ 1 β 3 |
13 |
|
3ne0 |
β’ 3 β 0 |
14 |
9 12 13
|
3pm3.2i |
β’ ( 0 β 1 β§ 1 β 3 β§ 3 β 0 ) |
15 |
|
c0ex |
β’ 0 β V |
16 |
|
1ex |
β’ 1 β V |
17 |
|
3ex |
β’ 3 β V |
18 |
|
hashtpg |
β’ ( ( 0 β V β§ 1 β V β§ 3 β V ) β ( ( 0 β 1 β§ 1 β 3 β§ 3 β 0 ) β ( β― β { 0 , 1 , 3 } ) = 3 ) ) |
19 |
15 16 17 18
|
mp3an |
β’ ( ( 0 β 1 β§ 1 β 3 β§ 3 β 0 ) β ( β― β { 0 , 1 , 3 } ) = 3 ) |
20 |
14 19
|
mpbi |
β’ ( β― β { 0 , 1 , 3 } ) = 3 |
21 |
20
|
breq1i |
β’ ( ( β― β { 0 , 1 , 3 } ) β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β 3 β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) ) |
22 |
|
df-3 |
β’ 3 = ( 2 + 1 ) |
23 |
22
|
breq1i |
β’ ( 3 β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β ( 2 + 1 ) β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) ) |
24 |
|
2z |
β’ 2 β β€ |
25 |
|
fzfi |
β’ ( 0 ... 3 ) β Fin |
26 |
1 25
|
eqeltri |
β’ π β Fin |
27 |
|
rabfi |
β’ ( π β Fin β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } β Fin ) |
28 |
|
hashcl |
β’ ( { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } β Fin β ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β β0 ) |
29 |
26 27 28
|
mp2b |
β’ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β β0 |
30 |
29
|
nn0zi |
β’ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β β€ |
31 |
|
zltp1le |
β’ ( ( 2 β β€ β§ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β β€ ) β ( 2 < ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β ( 2 + 1 ) β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) ) ) |
32 |
24 30 31
|
mp2an |
β’ ( 2 < ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β ( 2 + 1 ) β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) ) |
33 |
23 32
|
sylbb2 |
β’ ( 3 β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β 2 < ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) ) |
34 |
21 33
|
sylbi |
β’ ( ( β― β { 0 , 1 , 3 } ) β€ ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) β 2 < ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) ) |
35 |
4 8 34
|
mp2b |
β’ 2 < ( β― β { π₯ β π β£ Β¬ 2 β₯ ( ( VtxDeg β πΊ ) β π₯ ) } ) |