Metamath Proof Explorer

Theorem konigsberglem1

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