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=⟨“01020312122323”⟩
konigsberg.g ⊢G=VE
Assertion konigsberglem3 ⊢VtxDeg⁡G⁡3=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 nn0fz0 ⊢3∈ℕ0↔3∈0…3
11 9 10 mpbi ⊢3∈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 ⊢3∈0…3∧∅=∅→VtxDeg⁡0…3∅⁡3=0
79 11 77 78 mp2an ⊢VtxDeg⁡0…3∅⁡3=0
80 0elfz ⊢3∈ℕ0→0∈0…3
81 9 80 ax-mp ⊢0∈0…3
82 3ne0 ⊢3≠0
83 82 necomi ⊢0≠3
84 1nn0 ⊢1∈ℕ0
85 1le3 ⊢1≤3
86 elfz2nn0 ⊢1∈0…3↔1∈ℕ0∧3∈ℕ0∧1≤3
87 84 9 85 86 mpbir3an ⊢1∈0…3
88 1re ⊢1∈ℝ
89 1lt3 ⊢1<3
90 88 89 ltneii ⊢1≠3
91 s0s1 ⊢⟨“01”⟩=∅++⟨“01”⟩
92 65 91 eqtri ⊢iEdg⁡0…3⟨“01”⟩=∅++⟨“01”⟩
93 73 11 75 76 79 63 81 83 87 90 92 vdegp1ai ⊢VtxDeg⁡0…3⟨“01”⟩⁡3=0
94 2nn0 ⊢2∈ℕ0
95 2re ⊢2∈ℝ
96 3re ⊢3∈ℝ
97 2lt3 ⊢2<3
98 95 96 97 ltleii ⊢2≤3
99 elfz2nn0 ⊢2∈0…3↔2∈ℕ0∧3∈ℕ0∧2≤3
100 94 9 98 99 mpbir3an ⊢2∈0…3
101 95 97 ltneii ⊢2≠3
102 df-s2 ⊢⟨“0102”⟩=⟨“01”⟩++⟨“02”⟩
103 55 102 eqtri ⊢iEdg⁡0…3⟨“0102”⟩=⟨“01”⟩++⟨“02”⟩
104 64 11 66 70 93 53 81 83 100 101 103 vdegp1ai ⊢VtxDeg⁡0…3⟨“0102”⟩⁡3=0
105 df-s3 ⊢⟨“010203”⟩=⟨“0102”⟩++⟨“03”⟩
106 45 105 eqtri ⊢iEdg⁡0…3⟨“010203”⟩=⟨“0102”⟩++⟨“03”⟩
107 54 11 56 60 104 43 81 83 106 vdegp1ci ⊢VtxDeg⁡0…3⟨“010203”⟩⁡3=0+1
108 0p1e1 ⊢0+1=1
109 107 108 eqtri ⊢VtxDeg⁡0…3⟨“010203”⟩⁡3=1
110 df-s4 ⊢⟨“01020312”⟩=⟨“010203”⟩++⟨“12”⟩
111 35 110 eqtri ⊢iEdg⁡0…3⟨“01020312”⟩=⟨“010203”⟩++⟨“12”⟩
112 44 11 46 50 109 33 87 90 100 101 111 vdegp1ai ⊢VtxDeg⁡0…3⟨“01020312”⟩⁡3=1
113 df-s5 ⊢⟨“0102031212”⟩=⟨“01020312”⟩++⟨“12”⟩
114 25 113 eqtri ⊢iEdg⁡0…3⟨“0102031212”⟩=⟨“01020312”⟩++⟨“12”⟩
115 34 11 36 40 112 23 87 90 100 101 114 vdegp1ai ⊢VtxDeg⁡0…3⟨“0102031212”⟩⁡3=1
116 df-s6 ⊢⟨“010203121223”⟩=⟨“0102031212”⟩++⟨“23”⟩
117 12 116 eqtri ⊢iEdg⁡0…3⟨“010203121223”⟩=⟨“0102031212”⟩++⟨“23”⟩
118 24 11 26 30 115 7 100 101 117 vdegp1ci ⊢VtxDeg⁡0…3⟨“010203121223”⟩⁡3=1+1
119 1p1e2 ⊢1+1=2
120 118 119 eqtri ⊢VtxDeg⁡0…3⟨“010203121223”⟩⁡3=2
121 1 2 3 konigsbergvtx ⊢Vtx⁡G=0…3
122 1 2 3 konigsbergiedg ⊢iEdg⁡G=⟨“01020312122323”⟩
123 122 15 eqtri ⊢iEdg⁡G=⟨“010203121223”⟩++⟨“23”⟩
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