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=⟨“01020312122323”⟩
konigsberg.g ⊢G=VE
Assertion konigsberglem2 ⊢VtxDeg⁡G⁡1=3

Proof

Step Hyp Ref Expression
1 konigsberg.v ⊢V=0…3
2 konigsberg.e ⊢E=⟨“01020312122323”⟩
3 konigsberg.g ⊢G=VE
4 ovex ⊢0…3∈V
5 s6cli ⊢⟨“010203121223”⟩∈WordV
6 5 elexi ⊢⟨“010203121223”⟩∈V
7 4 6 opvtxfvi ⊢Vtx⁡0…3⟨“010203121223”⟩=0…3
8 7 eqcomi ⊢0…3=Vtx⁡0…3⟨“010203121223”⟩
9 1nn0 ⊢1∈ℕ0
10 3nn0 ⊢3∈ℕ0
11 1le3 ⊢1≤3
12 elfz2nn0 ⊢1∈0…3↔1∈ℕ0∧3∈ℕ0∧1≤3
13 9 10 11 12 mpbir3an ⊢1∈0…3
14 4 6 opiedgfvi ⊢iEdg⁡0…3⟨“010203121223”⟩=⟨“010203121223”⟩
15 14 eqcomi ⊢⟨“010203121223”⟩=iEdg⁡0…3⟨“010203121223”⟩
16 s1cli ⊢⟨“23”⟩∈WordV
17 df-s7 ⊢⟨“01020312122323”⟩=⟨“010203121223”⟩++⟨“23”⟩
18 eqid ⊢0…3=0…3
19 eqid ⊢⟨“01020312122323”⟩=⟨“01020312122323”⟩
20 eqid ⊢0…3⟨“01020312122323”⟩=0…3⟨“01020312122323”⟩
21 18 19 20 konigsbergssiedgw ⊢⟨“010203121223”⟩∈WordV∧⟨“23”⟩∈WordV∧⟨“01020312122323”⟩=⟨“010203121223”⟩++⟨“23”⟩→⟨“010203121223”⟩∈Wordx∈𝒫0…3∖∅|x≤2
22 5 16 17 21 mp3an ⊢⟨“010203121223”⟩∈Wordx∈𝒫0…3∖∅|x≤2
23 s5cli ⊢⟨“0102031212”⟩∈WordV
24 23 elexi ⊢⟨“0102031212”⟩∈V
25 4 24 opvtxfvi ⊢Vtx⁡0…3⟨“0102031212”⟩=0…3
26 25 eqcomi ⊢0…3=Vtx⁡0…3⟨“0102031212”⟩
27 4 24 opiedgfvi ⊢iEdg⁡0…3⟨“0102031212”⟩=⟨“0102031212”⟩
28 27 eqcomi ⊢⟨“0102031212”⟩=iEdg⁡0…3⟨“0102031212”⟩
29 s2cli ⊢⟨“2323”⟩∈WordV
30 s5s2 ⊢⟨“01020312122323”⟩=⟨“0102031212”⟩++⟨“2323”⟩
31 18 19 20 konigsbergssiedgw ⊢⟨“0102031212”⟩∈WordV∧⟨“2323”⟩∈WordV∧⟨“01020312122323”⟩=⟨“0102031212”⟩++⟨“2323”⟩→⟨“0102031212”⟩∈Wordx∈𝒫0…3∖∅|x≤2
32 23 29 30 31 mp3an ⊢⟨“0102031212”⟩∈Wordx∈𝒫0…3∖∅|x≤2
33 s4cli ⊢⟨“01020312”⟩∈WordV
34 33 elexi ⊢⟨“01020312”⟩∈V
35 4 34 opvtxfvi ⊢Vtx⁡0…3⟨“01020312”⟩=0…3
36 35 eqcomi ⊢0…3=Vtx⁡0…3⟨“01020312”⟩
37 4 34 opiedgfvi ⊢iEdg⁡0…3⟨“01020312”⟩=⟨“01020312”⟩
38 37 eqcomi ⊢⟨“01020312”⟩=iEdg⁡0…3⟨“01020312”⟩
39 s3cli ⊢⟨“122323”⟩∈WordV
40 s4s3 ⊢⟨“01020312122323”⟩=⟨“01020312”⟩++⟨“122323”⟩
41 18 19 20 konigsbergssiedgw ⊢⟨“01020312”⟩∈WordV∧⟨“122323”⟩∈WordV∧⟨“01020312122323”⟩=⟨“01020312”⟩++⟨“122323”⟩→⟨“01020312”⟩∈Wordx∈𝒫0…3∖∅|x≤2
42 33 39 40 41 mp3an ⊢⟨“01020312”⟩∈Wordx∈𝒫0…3∖∅|x≤2
43 s3cli ⊢⟨“010203”⟩∈WordV
44 43 elexi ⊢⟨“010203”⟩∈V
45 4 44 opvtxfvi ⊢Vtx⁡0…3⟨“010203”⟩=0…3
46 45 eqcomi ⊢0…3=Vtx⁡0…3⟨“010203”⟩
47 4 44 opiedgfvi ⊢iEdg⁡0…3⟨“010203”⟩=⟨“010203”⟩
48 47 eqcomi ⊢⟨“010203”⟩=iEdg⁡0…3⟨“010203”⟩
49 s4cli ⊢⟨“12122323”⟩∈WordV
50 s3s4 ⊢⟨“01020312122323”⟩=⟨“010203”⟩++⟨“12122323”⟩
51 18 19 20 konigsbergssiedgw ⊢⟨“010203”⟩∈WordV∧⟨“12122323”⟩∈WordV∧⟨“01020312122323”⟩=⟨“010203”⟩++⟨“12122323”⟩→⟨“010203”⟩∈Wordx∈𝒫0…3∖∅|x≤2
52 43 49 50 51 mp3an ⊢⟨“010203”⟩∈Wordx∈𝒫0…3∖∅|x≤2
53 s2cli ⊢⟨“0102”⟩∈WordV
54 53 elexi ⊢⟨“0102”⟩∈V
55 4 54 opvtxfvi ⊢Vtx⁡0…3⟨“0102”⟩=0…3
56 55 eqcomi ⊢0…3=Vtx⁡0…3⟨“0102”⟩
57 4 54 opiedgfvi ⊢iEdg⁡0…3⟨“0102”⟩=⟨“0102”⟩
58 57 eqcomi ⊢⟨“0102”⟩=iEdg⁡0…3⟨“0102”⟩
59 s5cli ⊢⟨“0312122323”⟩∈WordV
60 s2s5 ⊢⟨“01020312122323”⟩=⟨“0102”⟩++⟨“0312122323”⟩
61 18 19 20 konigsbergssiedgw ⊢⟨“0102”⟩∈WordV∧⟨“0312122323”⟩∈WordV∧⟨“01020312122323”⟩=⟨“0102”⟩++⟨“0312122323”⟩→⟨“0102”⟩∈Wordx∈𝒫0…3∖∅|x≤2
62 53 59 60 61 mp3an ⊢⟨“0102”⟩∈Wordx∈𝒫0…3∖∅|x≤2
63 s1cli ⊢⟨“01”⟩∈WordV
64 63 elexi ⊢⟨“01”⟩∈V
65 4 64 opvtxfvi ⊢Vtx⁡0…3⟨“01”⟩=0…3
66 65 eqcomi ⊢0…3=Vtx⁡0…3⟨“01”⟩
67 4 64 opiedgfvi ⊢iEdg⁡0…3⟨“01”⟩=⟨“01”⟩
68 67 eqcomi ⊢⟨“01”⟩=iEdg⁡0…3⟨“01”⟩
69 s6cli ⊢⟨“020312122323”⟩∈WordV
70 s1s6 ⊢⟨“01020312122323”⟩=⟨“01”⟩++⟨“020312122323”⟩
71 18 19 20 konigsbergssiedgw ⊢⟨“01”⟩∈WordV∧⟨“020312122323”⟩∈WordV∧⟨“01020312122323”⟩=⟨“01”⟩++⟨“020312122323”⟩→⟨“01”⟩∈Wordx∈𝒫0…3∖∅|x≤2
72 63 69 70 71 mp3an ⊢⟨“01”⟩∈Wordx∈𝒫0…3∖∅|x≤2
73 0ex ⊢∅∈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 ⊢∅∈Wordx∈𝒫0…3∖∅|x≤2
79 eqid ⊢∅=∅
80 75 77 vtxdg0e ⊢1∈0…3∧∅=∅→VtxDeg⁡0…3∅⁡1=0
81 13 79 80 mp2an ⊢VtxDeg⁡0…3∅⁡1=0
82 0elfz ⊢3∈ℕ0→0∈0…3
83 10 82 ax-mp ⊢0∈0…3
84 0ne1 ⊢0≠1
85 s0s1 ⊢⟨“01”⟩=∅++⟨“01”⟩
86 67 85 eqtri ⊢iEdg⁡0…3⟨“01”⟩=∅++⟨“01”⟩
87 75 13 77 78 81 65 83 84 86 vdegp1ci ⊢VtxDeg⁡0…3⟨“01”⟩⁡1=0+1
88 0p1e1 ⊢0+1=1
89 87 88 eqtri ⊢VtxDeg⁡0…3⟨“01”⟩⁡1=1
90 2nn0 ⊢2∈ℕ0
91 2re ⊢2∈ℝ
92 3re ⊢3∈ℝ
93 2lt3 ⊢2<3
94 91 92 93 ltleii ⊢2≤3
95 elfz2nn0 ⊢2∈0…3↔2∈ℕ0∧3∈ℕ0∧2≤3
96 90 10 94 95 mpbir3an ⊢2∈0…3
97 1ne2 ⊢1≠2
98 97 necomi ⊢2≠1
99 df-s2 ⊢⟨“0102”⟩=⟨“01”⟩++⟨“02”⟩
100 57 99 eqtri ⊢iEdg⁡0…3⟨“0102”⟩=⟨“01”⟩++⟨“02”⟩
101 66 13 68 72 89 55 83 84 96 98 100 vdegp1ai ⊢VtxDeg⁡0…3⟨“0102”⟩⁡1=1
102 nn0fz0 ⊢3∈ℕ0↔3∈0…3
103 10 102 mpbi ⊢3∈0…3
104 1re ⊢1∈ℝ
105 1lt3 ⊢1<3
106 104 105 gtneii ⊢3≠1
107 df-s3 ⊢⟨“010203”⟩=⟨“0102”⟩++⟨“03”⟩
108 47 107 eqtri ⊢iEdg⁡0…3⟨“010203”⟩=⟨“0102”⟩++⟨“03”⟩
109 56 13 58 62 101 45 83 84 103 106 108 vdegp1ai ⊢VtxDeg⁡0…3⟨“010203”⟩⁡1=1
110 df-s4 ⊢⟨“01020312”⟩=⟨“010203”⟩++⟨“12”⟩
111 37 110 eqtri ⊢iEdg⁡0…3⟨“01020312”⟩=⟨“010203”⟩++⟨“12”⟩
112 46 13 48 52 109 35 96 98 111 vdegp1bi ⊢VtxDeg⁡0…3⟨“01020312”⟩⁡1=1+1
113 1p1e2 ⊢1+1=2
114 112 113 eqtri ⊢VtxDeg⁡0…3⟨“01020312”⟩⁡1=2
115 df-s5 ⊢⟨“0102031212”⟩=⟨“01020312”⟩++⟨“12”⟩
116 27 115 eqtri ⊢iEdg⁡0…3⟨“0102031212”⟩=⟨“01020312”⟩++⟨“12”⟩
117 36 13 38 42 114 25 96 98 116 vdegp1bi ⊢VtxDeg⁡0…3⟨“0102031212”⟩⁡1=2+1
118 2p1e3 ⊢2+1=3
119 117 118 eqtri ⊢VtxDeg⁡0…3⟨“0102031212”⟩⁡1=3
120 df-s6 ⊢⟨“010203121223”⟩=⟨“0102031212”⟩++⟨“23”⟩
121 14 120 eqtri ⊢iEdg⁡0…3⟨“010203121223”⟩=⟨“0102031212”⟩++⟨“23”⟩
122 26 13 28 32 119 7 96 98 103 106 121 vdegp1ai ⊢VtxDeg⁡0…3⟨“010203121223”⟩⁡1=3
123 1 2 3 konigsbergvtx ⊢Vtx⁡G=0…3
124 1 2 3 konigsbergiedg ⊢iEdg⁡G=⟨“01020312122323”⟩
125 124 17 eqtri ⊢iEdg⁡G=⟨“010203121223”⟩++⟨“23”⟩
126 8 13 15 22 122 123 96 98 103 106 125 vdegp1ai ⊢VtxDeg⁡G⁡1=3