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