Step | Hyp | Ref
| Expression |
1 | | ovex 7391 |
. . . 4
β’ (0...3)
β V |
2 | | s6cli 14774 |
. . . . 5
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}ββ©
β Word V |
3 | 2 | elexi 3465 |
. . . 4
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}ββ©
β V |
4 | 1, 3 | opvtxfvi 27963 |
. . 3
β’
(Vtxββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2} {2, 3}ββ©β©) = (0...3) |
5 | 4 | eqcomi 2746 |
. 2
β’ (0...3) =
(Vtxββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2,
3}ββ©β©) |
6 | | 3nn0 12432 |
. . 3
β’ 3 β
β0 |
7 | | 0elfz 13539 |
. . 3
β’ (3 β
β0 β 0 β (0...3)) |
8 | 6, 7 | ax-mp 5 |
. 2
β’ 0 β
(0...3) |
9 | 1, 3 | opiedgfvi 27964 |
. . 3
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2} {2, 3}ββ©β©) = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}
{2, 3}ββ© |
10 | 9 | eqcomi 2746 |
. 2
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}ββ© =
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2,
3}ββ©β©) |
11 | | s1cli 14494 |
. . 3
β’
β¨β{2, 3}ββ© β Word V |
12 | | df-s7 14743 |
. . 3
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© = (β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2,
3}ββ© ++ β¨β{2, 3}ββ©) |
13 | | eqid 2737 |
. . . 4
β’ (0...3) =
(0...3) |
14 | | eqid 2737 |
. . . 4
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© |
15 | | eqid 2737 |
. . . 4
β’
β¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}
{2, 3}ββ©β© = β¨(0...3), β¨β{0, 1} {0, 2} {0, 3}
{1, 2} {1, 2} {2, 3} {2, 3}ββ©β© |
16 | 13, 14, 15 | konigsbergssiedgw 29197 |
. . 3
β’
((β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}ββ©
β Word V β§ β¨β{2, 3}ββ© β Word V β§
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© =
(β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}ββ© ++
β¨β{2, 3}ββ©)) β β¨β{0, 1} {0, 2} {0, 3} {1,
2} {1, 2} {2, 3}ββ© β Word {π₯ β (π« (0...3) β {β
})
β£ (β―βπ₯)
β€ 2}) |
17 | 2, 11, 12, 16 | mp3an 1462 |
. 2
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}ββ©
β Word {π₯ β
(π« (0...3) β {β
}) β£ (β―βπ₯) β€ 2} |
18 | | s5cli 14773 |
. . . . . 6
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}ββ© β Word
V |
19 | 18 | elexi 3465 |
. . . . 5
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}ββ© β
V |
20 | 1, 19 | opvtxfvi 27963 |
. . . 4
β’
(Vtxββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2}ββ©β©) = (0...3) |
21 | 20 | eqcomi 2746 |
. . 3
β’ (0...3) =
(Vtxββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2}ββ©β©) |
22 | 1, 19 | opiedgfvi 27964 |
. . . 4
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2}ββ©β©) = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2}ββ© |
23 | 22 | eqcomi 2746 |
. . 3
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}ββ© =
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2}ββ©β©) |
24 | | s2cli 14770 |
. . . 4
β’
β¨β{2, 3} {2, 3}ββ© β Word V |
25 | | s5s2 14825 |
. . . 4
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© = (β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}ββ©
++ β¨β{2, 3} {2, 3}ββ©) |
26 | 13, 14, 15 | konigsbergssiedgw 29197 |
. . . 4
β’
((β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}ββ© β
Word V β§ β¨β{2, 3} {2, 3}ββ© β Word V β§
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© =
(β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}ββ© ++
β¨β{2, 3} {2, 3}ββ©)) β β¨β{0, 1} {0, 2} {0,
3} {1, 2} {1, 2}ββ© β Word {π₯ β (π« (0...3) β {β
})
β£ (β―βπ₯)
β€ 2}) |
27 | 18, 24, 25, 26 | mp3an 1462 |
. . 3
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}ββ© β Word
{π₯ β (π«
(0...3) β {β
}) β£ (β―βπ₯) β€ 2} |
28 | | s4cli 14772 |
. . . . . . 7
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ© β Word
V |
29 | 28 | elexi 3465 |
. . . . . 6
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ© β
V |
30 | 1, 29 | opvtxfvi 27963 |
. . . . 5
β’
(Vtxββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1,
2}ββ©β©) = (0...3) |
31 | 30 | eqcomi 2746 |
. . . 4
β’ (0...3) =
(Vtxββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1,
2}ββ©β©) |
32 | 1, 29 | opiedgfvi 27964 |
. . . . 5
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1,
2}ββ©β©) = β¨β{0, 1} {0, 2} {0, 3} {1,
2}ββ© |
33 | 32 | eqcomi 2746 |
. . . 4
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ© =
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1,
2}ββ©β©) |
34 | | s3cli 14771 |
. . . . 5
β’
β¨β{1, 2} {2, 3} {2, 3}ββ© β Word
V |
35 | | s4s3 14821 |
. . . . 5
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© = (β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ© ++
β¨β{1, 2} {2, 3} {2, 3}ββ©) |
36 | 13, 14, 15 | konigsbergssiedgw 29197 |
. . . . 5
β’
((β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ© β Word V
β§ β¨β{1, 2} {2, 3} {2, 3}ββ© β Word V β§
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© =
(β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ© ++ β¨β{1, 2}
{2, 3} {2, 3}ββ©)) β β¨β{0, 1} {0, 2} {0, 3} {1,
2}ββ© β Word {π₯ β (π« (0...3) β {β
})
β£ (β―βπ₯)
β€ 2}) |
37 | 28, 34, 35, 36 | mp3an 1462 |
. . . 4
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ© β Word {π₯ β (π« (0...3)
β {β
}) β£ (β―βπ₯) β€ 2} |
38 | | s3cli 14771 |
. . . . . . . 8
β’
β¨β{0, 1} {0, 2} {0, 3}ββ© β Word
V |
39 | 38 | elexi 3465 |
. . . . . . 7
β’
β¨β{0, 1} {0, 2} {0, 3}ββ© β V |
40 | 1, 39 | opvtxfvi 27963 |
. . . . . 6
β’
(Vtxββ¨(0...3), β¨β{0, 1} {0, 2} {0,
3}ββ©β©) = (0...3) |
41 | 40 | eqcomi 2746 |
. . . . 5
β’ (0...3) =
(Vtxββ¨(0...3), β¨β{0, 1} {0, 2} {0,
3}ββ©β©) |
42 | 1, 39 | opiedgfvi 27964 |
. . . . . 6
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0,
3}ββ©β©) = β¨β{0, 1} {0, 2} {0,
3}ββ© |
43 | 42 | eqcomi 2746 |
. . . . 5
β’
β¨β{0, 1} {0, 2} {0, 3}ββ© =
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0,
3}ββ©β©) |
44 | | s4cli 14772 |
. . . . . 6
β’
β¨β{1, 2} {1, 2} {2, 3} {2, 3}ββ© β Word
V |
45 | | s3s4 14823 |
. . . . . 6
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© = (β¨β{0, 1} {0, 2} {0, 3}ββ© ++
β¨β{1, 2} {1, 2} {2, 3} {2, 3}ββ©) |
46 | 13, 14, 15 | konigsbergssiedgw 29197 |
. . . . . 6
β’
((β¨β{0, 1} {0, 2} {0, 3}ββ© β Word V β§
β¨β{1, 2} {1, 2} {2, 3} {2, 3}ββ© β Word V β§
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© =
(β¨β{0, 1} {0, 2} {0, 3}ββ© ++ β¨β{1, 2} {1, 2}
{2, 3} {2, 3}ββ©)) β β¨β{0, 1} {0, 2} {0,
3}ββ© β Word {π₯ β (π« (0...3) β {β
})
β£ (β―βπ₯)
β€ 2}) |
47 | 38, 44, 45, 46 | mp3an 1462 |
. . . . 5
β’
β¨β{0, 1} {0, 2} {0, 3}ββ© β Word {π₯ β (π« (0...3)
β {β
}) β£ (β―βπ₯) β€ 2} |
48 | | s2cli 14770 |
. . . . . . . . . 10
β’
β¨β{0, 1} {0, 2}ββ© β Word V |
49 | 48 | elexi 3465 |
. . . . . . . . 9
β’
β¨β{0, 1} {0, 2}ββ© β V |
50 | 1, 49 | opvtxfvi 27963 |
. . . . . . . 8
β’
(Vtxββ¨(0...3), β¨β{0, 1} {0, 2}ββ©β©)
= (0...3) |
51 | 50 | eqcomi 2746 |
. . . . . . 7
β’ (0...3) =
(Vtxββ¨(0...3), β¨β{0, 1} {0,
2}ββ©β©) |
52 | 1, 49 | opiedgfvi 27964 |
. . . . . . . 8
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0,
2}ββ©β©) = β¨β{0, 1} {0,
2}ββ© |
53 | 52 | eqcomi 2746 |
. . . . . . 7
β’
β¨β{0, 1} {0, 2}ββ© = (iEdgββ¨(0...3),
β¨β{0, 1} {0, 2}ββ©β©) |
54 | | s5cli 14773 |
. . . . . . . 8
β’
β¨β{0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© β Word
V |
55 | | s2s5 14824 |
. . . . . . . 8
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© = (β¨β{0, 1} {0, 2}ββ© ++ β¨β{0,
3} {1, 2} {1, 2} {2, 3} {2, 3}ββ©) |
56 | 13, 14, 15 | konigsbergssiedgw 29197 |
. . . . . . . 8
β’
((β¨β{0, 1} {0, 2}ββ© β Word V β§
β¨β{0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© β Word V
β§ β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© = (β¨β{0, 1} {0, 2}ββ© ++ β¨β{0,
3} {1, 2} {1, 2} {2, 3} {2, 3}ββ©)) β β¨β{0, 1} {0,
2}ββ© β Word {π₯ β (π« (0...3) β {β
})
β£ (β―βπ₯)
β€ 2}) |
57 | 48, 54, 55, 56 | mp3an 1462 |
. . . . . . 7
β’
β¨β{0, 1} {0, 2}ββ© β Word {π₯ β (π« (0...3) β {β
})
β£ (β―βπ₯)
β€ 2} |
58 | | s1cli 14494 |
. . . . . . . . . . . 12
β’
β¨β{0, 1}ββ© β Word V |
59 | 58 | elexi 3465 |
. . . . . . . . . . 11
β’
β¨β{0, 1}ββ© β V |
60 | 1, 59 | opvtxfvi 27963 |
. . . . . . . . . 10
β’
(Vtxββ¨(0...3), β¨β{0, 1}ββ©β©) =
(0...3) |
61 | 60 | eqcomi 2746 |
. . . . . . . . 9
β’ (0...3) =
(Vtxββ¨(0...3), β¨β{0,
1}ββ©β©) |
62 | 1, 59 | opiedgfvi 27964 |
. . . . . . . . . 10
β’
(iEdgββ¨(0...3), β¨β{0, 1}ββ©β©) =
β¨β{0, 1}ββ© |
63 | 62 | eqcomi 2746 |
. . . . . . . . 9
β’
β¨β{0, 1}ββ© = (iEdgββ¨(0...3),
β¨β{0, 1}ββ©β©) |
64 | | s6cli 14774 |
. . . . . . . . . 10
β’
β¨β{0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ©
β Word V |
65 | | s1s6 14817 |
. . . . . . . . . 10
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© = (β¨β{0, 1}ββ© ++ β¨β{0, 2} {0,
3} {1, 2} {1, 2} {2, 3} {2, 3}ββ©) |
66 | 13, 14, 15 | konigsbergssiedgw 29197 |
. . . . . . . . . 10
β’
((β¨β{0, 1}ββ© β Word V β§ β¨β{0,
2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© β Word V β§
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© =
(β¨β{0, 1}ββ© ++ β¨β{0, 2} {0, 3} {1, 2} {1, 2}
{2, 3} {2, 3}ββ©)) β β¨β{0, 1}ββ© β
Word {π₯ β (π«
(0...3) β {β
}) β£ (β―βπ₯) β€ 2}) |
67 | 58, 64, 65, 66 | mp3an 1462 |
. . . . . . . . 9
β’
β¨β{0, 1}ββ© β Word {π₯ β (π« (0...3) β {β
})
β£ (β―βπ₯)
β€ 2} |
68 | | 0ex 5265 |
. . . . . . . . . . . . 13
β’ β
β V |
69 | 1, 68 | opvtxfvi 27963 |
. . . . . . . . . . . 12
β’
(Vtxββ¨(0...3), β
β©) = (0...3) |
70 | 69 | eqcomi 2746 |
. . . . . . . . . . 11
β’ (0...3) =
(Vtxββ¨(0...3), β
β©) |
71 | 1, 68 | opiedgfvi 27964 |
. . . . . . . . . . . 12
β’
(iEdgββ¨(0...3), β
β©) = β
|
72 | 71 | eqcomi 2746 |
. . . . . . . . . . 11
β’ β
=
(iEdgββ¨(0...3), β
β©) |
73 | | wrd0 14428 |
. . . . . . . . . . 11
β’ β
β Word {π₯ β
(π« (0...3) β {β
}) β£ (β―βπ₯) β€ 2} |
74 | | eqid 2737 |
. . . . . . . . . . . 12
β’ β
=
β
|
75 | 70, 72 | vtxdg0e 28425 |
. . . . . . . . . . . 12
β’ ((0
β (0...3) β§ β
= β
) β ((VtxDegββ¨(0...3),
β
β©)β0) = 0) |
76 | 8, 74, 75 | mp2an 691 |
. . . . . . . . . . 11
β’
((VtxDegββ¨(0...3), β
β©)β0) =
0 |
77 | | 1nn0 12430 |
. . . . . . . . . . . 12
β’ 1 β
β0 |
78 | | 1le3 12366 |
. . . . . . . . . . . 12
β’ 1 β€
3 |
79 | | elfz2nn0 13533 |
. . . . . . . . . . . 12
β’ (1 β
(0...3) β (1 β β0 β§ 3 β β0
β§ 1 β€ 3)) |
80 | 77, 6, 78, 79 | mpbir3an 1342 |
. . . . . . . . . . 11
β’ 1 β
(0...3) |
81 | | ax-1ne0 11121 |
. . . . . . . . . . 11
β’ 1 β
0 |
82 | | s0s1 14812 |
. . . . . . . . . . . 12
β’
β¨β{0, 1}ββ© = (β
++ β¨β{0,
1}ββ©) |
83 | 62, 82 | eqtri 2765 |
. . . . . . . . . . 11
β’
(iEdgββ¨(0...3), β¨β{0, 1}ββ©β©) =
(β
++ β¨β{0, 1}ββ©) |
84 | 70, 8, 72, 73, 76, 60, 80, 81, 83 | vdegp1bi 28488 |
. . . . . . . . . 10
β’
((VtxDegββ¨(0...3), β¨β{0,
1}ββ©β©)β0) = (0 + 1) |
85 | | 0p1e1 12276 |
. . . . . . . . . 10
β’ (0 + 1) =
1 |
86 | 84, 85 | eqtri 2765 |
. . . . . . . . 9
β’
((VtxDegββ¨(0...3), β¨β{0,
1}ββ©β©)β0) = 1 |
87 | | 2nn0 12431 |
. . . . . . . . . 10
β’ 2 β
β0 |
88 | | 2re 12228 |
. . . . . . . . . . 11
β’ 2 β
β |
89 | | 3re 12234 |
. . . . . . . . . . 11
β’ 3 β
β |
90 | | 2lt3 12326 |
. . . . . . . . . . 11
β’ 2 <
3 |
91 | 88, 89, 90 | ltleii 11279 |
. . . . . . . . . 10
β’ 2 β€
3 |
92 | | elfz2nn0 13533 |
. . . . . . . . . 10
β’ (2 β
(0...3) β (2 β β0 β§ 3 β β0
β§ 2 β€ 3)) |
93 | 87, 6, 91, 92 | mpbir3an 1342 |
. . . . . . . . 9
β’ 2 β
(0...3) |
94 | | 2ne0 12258 |
. . . . . . . . 9
β’ 2 β
0 |
95 | | df-s2 14738 |
. . . . . . . . . 10
β’
β¨β{0, 1} {0, 2}ββ© = (β¨β{0,
1}ββ© ++ β¨β{0, 2}ββ©) |
96 | 52, 95 | eqtri 2765 |
. . . . . . . . 9
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0,
2}ββ©β©) = (β¨β{0, 1}ββ© ++ β¨β{0,
2}ββ©) |
97 | 61, 8, 63, 67, 86, 50, 93, 94, 96 | vdegp1bi 28488 |
. . . . . . . 8
β’
((VtxDegββ¨(0...3), β¨β{0, 1} {0,
2}ββ©β©)β0) = (1 + 1) |
98 | | 1p1e2 12279 |
. . . . . . . 8
β’ (1 + 1) =
2 |
99 | 97, 98 | eqtri 2765 |
. . . . . . 7
β’
((VtxDegββ¨(0...3), β¨β{0, 1} {0,
2}ββ©β©)β0) = 2 |
100 | | nn0fz0 13540 |
. . . . . . . 8
β’ (3 β
β0 β 3 β (0...3)) |
101 | 6, 100 | mpbi 229 |
. . . . . . 7
β’ 3 β
(0...3) |
102 | | 3ne0 12260 |
. . . . . . 7
β’ 3 β
0 |
103 | | df-s3 14739 |
. . . . . . . 8
β’
β¨β{0, 1} {0, 2} {0, 3}ββ© = (β¨β{0, 1}
{0, 2}ββ© ++ β¨β{0, 3}ββ©) |
104 | 42, 103 | eqtri 2765 |
. . . . . . 7
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0,
3}ββ©β©) = (β¨β{0, 1} {0, 2}ββ© ++
β¨β{0, 3}ββ©) |
105 | 51, 8, 53, 57, 99, 40, 101, 102, 104 | vdegp1bi 28488 |
. . . . . 6
β’
((VtxDegββ¨(0...3), β¨β{0, 1} {0, 2} {0,
3}ββ©β©)β0) = (2 + 1) |
106 | | 2p1e3 12296 |
. . . . . 6
β’ (2 + 1) =
3 |
107 | 105, 106 | eqtri 2765 |
. . . . 5
β’
((VtxDegββ¨(0...3), β¨β{0, 1} {0, 2} {0,
3}ββ©β©)β0) = 3 |
108 | | df-s4 14740 |
. . . . . 6
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ© =
(β¨β{0, 1} {0, 2} {0, 3}ββ© ++ β¨β{1,
2}ββ©) |
109 | 32, 108 | eqtri 2765 |
. . . . 5
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1,
2}ββ©β©) = (β¨β{0, 1} {0, 2} {0, 3}ββ© ++
β¨β{1, 2}ββ©) |
110 | 41, 8, 43, 47, 107, 30, 80, 81, 93, 94, 109 | vdegp1ai 28487 |
. . . 4
β’
((VtxDegββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1,
2}ββ©β©)β0) = 3 |
111 | | df-s5 14741 |
. . . . 5
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}ββ© =
(β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ© ++ β¨β{1,
2}ββ©) |
112 | 22, 111 | eqtri 2765 |
. . . 4
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2}ββ©β©) = (β¨β{0, 1} {0, 2} {0, 3} {1, 2}ββ©
++ β¨β{1, 2}ββ©) |
113 | 31, 8, 33, 37, 110, 20, 80, 81, 93, 94, 112 | vdegp1ai 28487 |
. . 3
β’
((VtxDegββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2}
{1, 2}ββ©β©)β0) = 3 |
114 | | df-s6 14742 |
. . . 4
β’
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}ββ© =
(β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}ββ© ++
β¨β{2, 3}ββ©) |
115 | 9, 114 | eqtri 2765 |
. . 3
β’
(iEdgββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2} {2, 3}ββ©β©) = (β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1,
2}ββ© ++ β¨β{2, 3}ββ©) |
116 | 21, 8, 23, 27, 113, 4, 93, 94, 101, 102, 115 | vdegp1ai 28487 |
. 2
β’
((VtxDegββ¨(0...3), β¨β{0, 1} {0, 2} {0, 3} {1, 2}
{1, 2} {2, 3}ββ©β©)β0) = 3 |
117 | | konigsberg.v |
. . 3
β’ π = (0...3) |
118 | | konigsberg.e |
. . 3
β’ πΈ = β¨β{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© |
119 | | konigsberg.g |
. . 3
β’ πΊ = β¨π, πΈβ© |
120 | 117, 118,
119 | konigsbergvtx 29193 |
. 2
β’
(VtxβπΊ) =
(0...3) |
121 | 117, 118,
119 | konigsbergiedg 29194 |
. . 3
β’
(iEdgβπΊ) =
β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2,
3}ββ© |
122 | 121, 12 | eqtri 2765 |
. 2
β’
(iEdgβπΊ) =
(β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}ββ© ++
β¨β{2, 3}ββ©) |
123 | 5, 8, 10, 17, 116, 120, 93, 94, 101, 102, 122 | vdegp1ai 28487 |
1
β’
((VtxDegβπΊ)β0) = 3 |