Metamath Proof Explorer

Theorem konigsberglem2

Description: Lemma 2 for konigsberg : Vertex 1 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 4-Mar-2021)

Ref Expression
Hypotheses konigsberg.v 
|- V = ( 0 ... 3 )
konigsberg.e 
|- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">
konigsberg.g 
|- G = <. V , E >.
Assertion konigsberglem2 
|- ( ( VtxDeg ` G ) ` 1 ) = 3

Proof

Step Hyp Ref Expression
1 konigsberg.v 
 |-  V = ( 0 ... 3 )
2 konigsberg.e 
 |-  E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">
3 konigsberg.g 
 |-  G = <. V , E >.
4 ovex 
 |-  ( 0 ... 3 ) e. _V
5 s6cli 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } "> e. Word _V
6 5 elexi 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } "> e. _V
7 4 6 opvtxfvi 
 |-  ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } "> >. ) = ( 0 ... 3 )
8 7 eqcomi 
 |-  ( 0 ... 3 ) = ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } "> >. )
9 1nn0 
 |-  1 e. NN0
10 3nn0 
 |-  3 e. NN0
11 1le3 
 |-  1 <_ 3
12 elfz2nn0 
 |-  ( 1 e. ( 0 ... 3 ) <-> ( 1 e. NN0 /\ 3 e. NN0 /\ 1 <_ 3 ) )
13 9 10 11 12 mpbir3an 
 |-  1 e. ( 0 ... 3 )
14 4 6 opiedgfvi 
 |-  ( 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 } ">
15 14 eqcomi 
 |-  <" { 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 } "> >. )
16 s1cli 
 |-  <" { 2 , 3 } "> e. Word _V
17 df-s7 
 |-  <" { 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 } "> )
18 eqid 
 |-  ( 0 ... 3 ) = ( 0 ... 3 )
19 eqid 
 |-  <" { 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 } ">
20 eqid 
 |-  <. ( 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 } "> >.
21 18 19 20 konigsbergssiedgw 
 |-  ( ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } "> e. Word _V /\ <" { 2 , 3 } "> e. 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 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 } )
22 5 16 17 21 mp3an 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 }
23 s5cli 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> e. Word _V
24 23 elexi 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> e. _V
25 4 24 opvtxfvi 
 |-  ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> >. ) = ( 0 ... 3 )
26 25 eqcomi 
 |-  ( 0 ... 3 ) = ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> >. )
27 4 24 opiedgfvi 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> >. ) = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ">
28 27 eqcomi 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> = ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> >. )
29 s2cli 
 |-  <" { 2 , 3 } { 2 , 3 } "> e. Word _V
30 s5s2 
 |-  <" { 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 } "> )
31 18 19 20 konigsbergssiedgw 
 |-  ( ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> e. Word _V /\ <" { 2 , 3 } { 2 , 3 } "> e. 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 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 } )
32 23 29 30 31 mp3an 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 }
33 s4cli 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> e. Word _V
34 33 elexi 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> e. _V
35 4 34 opvtxfvi 
 |-  ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> >. ) = ( 0 ... 3 )
36 35 eqcomi 
 |-  ( 0 ... 3 ) = ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> >. )
37 4 34 opiedgfvi 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> >. ) = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ">
38 37 eqcomi 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> = ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> >. )
39 s3cli 
 |-  <" { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. Word _V
40 s4s3 
 |-  <" { 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 } "> )
41 18 19 20 konigsbergssiedgw 
 |-  ( ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> e. Word _V /\ <" { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. 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 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 } )
42 33 39 40 41 mp3an 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 }
43 s3cli 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> e. Word _V
44 43 elexi 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> e. _V
45 4 44 opvtxfvi 
 |-  ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> >. ) = ( 0 ... 3 )
46 45 eqcomi 
 |-  ( 0 ... 3 ) = ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> >. )
47 4 44 opiedgfvi 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> >. ) = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } ">
48 47 eqcomi 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> = ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> >. )
49 s4cli 
 |-  <" { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. Word _V
50 s3s4 
 |-  <" { 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 } "> )
51 18 19 20 konigsbergssiedgw 
 |-  ( ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> e. Word _V /\ <" { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. 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 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 } )
52 43 49 50 51 mp3an 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 }
53 s2cli 
 |-  <" { 0 , 1 } { 0 , 2 } "> e. Word _V
54 53 elexi 
 |-  <" { 0 , 1 } { 0 , 2 } "> e. _V
55 4 54 opvtxfvi 
 |-  ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } "> >. ) = ( 0 ... 3 )
56 55 eqcomi 
 |-  ( 0 ... 3 ) = ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } "> >. )
57 4 54 opiedgfvi 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } "> >. ) = <" { 0 , 1 } { 0 , 2 } ">
58 57 eqcomi 
 |-  <" { 0 , 1 } { 0 , 2 } "> = ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } "> >. )
59 s5cli 
 |-  <" { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. Word _V
60 s2s5 
 |-  <" { 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 } "> )
61 18 19 20 konigsbergssiedgw 
 |-  ( ( <" { 0 , 1 } { 0 , 2 } "> e. Word _V /\ <" { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. 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 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 } )
62 53 59 60 61 mp3an 
 |-  <" { 0 , 1 } { 0 , 2 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 }
63 s1cli 
 |-  <" { 0 , 1 } "> e. Word _V
64 63 elexi 
 |-  <" { 0 , 1 } "> e. _V
65 4 64 opvtxfvi 
 |-  ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } "> >. ) = ( 0 ... 3 )
66 65 eqcomi 
 |-  ( 0 ... 3 ) = ( Vtx ` <. ( 0 ... 3 ) , <" { 0 , 1 } "> >. )
67 4 64 opiedgfvi 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } "> >. ) = <" { 0 , 1 } ">
68 67 eqcomi 
 |-  <" { 0 , 1 } "> = ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } "> >. )
69 s6cli 
 |-  <" { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. Word _V
70 s1s6 
 |-  <" { 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 } "> )
71 18 19 20 konigsbergssiedgw 
 |-  ( ( <" { 0 , 1 } "> e. Word _V /\ <" { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. 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 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 } )
72 63 69 70 71 mp3an 
 |-  <" { 0 , 1 } "> e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 }
73 0ex 
 |-  (/) e. _V
74 4 73 opvtxfvi 
 |-  ( Vtx ` <. ( 0 ... 3 ) , (/) >. ) = ( 0 ... 3 )
75 74 eqcomi 
 |-  ( 0 ... 3 ) = ( Vtx ` <. ( 0 ... 3 ) , (/) >. )
76 4 73 opiedgfvi 
 |-  ( iEdg ` <. ( 0 ... 3 ) , (/) >. ) = (/)
77 76 eqcomi 
 |-  (/) = ( iEdg ` <. ( 0 ... 3 ) , (/) >. )
78 wrd0 
 |-  (/) e. Word { x e. ( ~P ( 0 ... 3 ) \ { (/) } ) | ( # ` x ) <_ 2 }
79 eqid 
 |-  (/) = (/)
80 75 77 vtxdg0e 
 |-  ( ( 1 e. ( 0 ... 3 ) /\ (/) = (/) ) -> ( ( VtxDeg ` <. ( 0 ... 3 ) , (/) >. ) ` 1 ) = 0 )
81 13 79 80 mp2an 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , (/) >. ) ` 1 ) = 0
82 0elfz 
 |-  ( 3 e. NN0 -> 0 e. ( 0 ... 3 ) )
83 10 82 ax-mp 
 |-  0 e. ( 0 ... 3 )
84 0ne1 
 |-  0 =/= 1
85 s0s1 
 |-  <" { 0 , 1 } "> = ( (/) ++ <" { 0 , 1 } "> )
86 67 85 eqtri 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } "> >. ) = ( (/) ++ <" { 0 , 1 } "> )
87 75 13 77 78 81 65 83 84 86 vdegp1ci 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , <" { 0 , 1 } "> >. ) ` 1 ) = ( 0 + 1 )
88 0p1e1 
 |-  ( 0 + 1 ) = 1
89 87 88 eqtri 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , <" { 0 , 1 } "> >. ) ` 1 ) = 1
90 2nn0 
 |-  2 e. NN0
91 2re 
 |-  2 e. RR
92 3re 
 |-  3 e. RR
93 2lt3 
 |-  2 < 3
94 91 92 93 ltleii 
 |-  2 <_ 3
95 elfz2nn0 
 |-  ( 2 e. ( 0 ... 3 ) <-> ( 2 e. NN0 /\ 3 e. NN0 /\ 2 <_ 3 ) )
96 90 10 94 95 mpbir3an 
 |-  2 e. ( 0 ... 3 )
97 1ne2 
 |-  1 =/= 2
98 97 necomi 
 |-  2 =/= 1
99 df-s2 
 |-  <" { 0 , 1 } { 0 , 2 } "> = ( <" { 0 , 1 } "> ++ <" { 0 , 2 } "> )
100 57 99 eqtri 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } "> >. ) = ( <" { 0 , 1 } "> ++ <" { 0 , 2 } "> )
101 66 13 68 72 89 55 83 84 96 98 100 vdegp1ai 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } "> >. ) ` 1 ) = 1
102 nn0fz0 
 |-  ( 3 e. NN0 <-> 3 e. ( 0 ... 3 ) )
103 10 102 mpbi 
 |-  3 e. ( 0 ... 3 )
104 1re 
 |-  1 e. RR
105 1lt3 
 |-  1 < 3
106 104 105 gtneii 
 |-  3 =/= 1
107 df-s3 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> = ( <" { 0 , 1 } { 0 , 2 } "> ++ <" { 0 , 3 } "> )
108 47 107 eqtri 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> >. ) = ( <" { 0 , 1 } { 0 , 2 } "> ++ <" { 0 , 3 } "> )
109 56 13 58 62 101 45 83 84 103 106 108 vdegp1ai 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> >. ) ` 1 ) = 1
110 df-s4 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> = ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> ++ <" { 1 , 2 } "> )
111 37 110 eqtri 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> >. ) = ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } "> ++ <" { 1 , 2 } "> )
112 46 13 48 52 109 35 96 98 111 vdegp1bi 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> >. ) ` 1 ) = ( 1 + 1 )
113 1p1e2 
 |-  ( 1 + 1 ) = 2
114 112 113 eqtri 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> >. ) ` 1 ) = 2
115 df-s5 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> = ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> ++ <" { 1 , 2 } "> )
116 27 115 eqtri 
 |-  ( iEdg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> >. ) = ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } "> ++ <" { 1 , 2 } "> )
117 36 13 38 42 114 25 96 98 116 vdegp1bi 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> >. ) ` 1 ) = ( 2 + 1 )
118 2p1e3 
 |-  ( 2 + 1 ) = 3
119 117 118 eqtri 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> >. ) ` 1 ) = 3
120 df-s6 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } "> = ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } "> ++ <" { 2 , 3 } "> )
121 14 120 eqtri 
 |-  ( 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 } "> )
122 26 13 28 32 119 7 96 98 103 106 121 vdegp1ai 
 |-  ( ( VtxDeg ` <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } "> >. ) ` 1 ) = 3
123 1 2 3 konigsbergvtx 
 |-  ( Vtx ` G ) = ( 0 ... 3 )
124 1 2 3 konigsbergiedg 
 |-  ( iEdg ` G ) = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">
125 124 17 eqtri 
 |-  ( iEdg ` G ) = ( <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } "> ++ <" { 2 , 3 } "> )
126 8 13 15 22 122 123 96 98 103 106 125 vdegp1ai 
 |-  ( ( VtxDeg ` G ) ` 1 ) = 3