Metamath Proof Explorer

Theorem konigsberglem3

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