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 ∈ V
5 s6cli ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 ”⟩ ∈ Word V
6 5 elexi ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 ”⟩ ∈ 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 ∈ ℕ 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 ⟨“ 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 ”⟩ ∈ 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 ”⟩ ∈ Word V ∧ ⟨“ 2 3 ”⟩ ∈ 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 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
22 5 16 17 21 mp3an ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
23 s5cli ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ ∈ Word V
24 23 elexi ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ Word V ∧ ⟨“ 2 3 2 3 ”⟩ ∈ 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 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
32 23 29 30 31 mp3an ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
33 s4cli ⊢ ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ∈ Word V
34 33 elexi ⊢ ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ Word V ∧ ⟨“ 1 2 2 3 2 3 ”⟩ ∈ 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 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
42 33 39 40 41 mp3an ⊢ ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
43 s3cli ⊢ ⟨“ 0 1 0 2 0 3 ”⟩ ∈ Word V
44 43 elexi ⊢ ⟨“ 0 1 0 2 0 3 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ Word V ∧ ⟨“ 1 2 1 2 2 3 2 3 ”⟩ ∈ 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 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
52 43 49 50 51 mp3an ⊢ ⟨“ 0 1 0 2 0 3 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
53 s2cli ⊢ ⟨“ 0 1 0 2 ”⟩ ∈ Word V
54 53 elexi ⊢ ⟨“ 0 1 0 2 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ Word V ∧ ⟨“ 0 3 1 2 1 2 2 3 2 3 ”⟩ ∈ 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 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
62 53 59 60 61 mp3an ⊢ ⟨“ 0 1 0 2 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
63 s1cli ⊢ ⟨“ 0 1 ”⟩ ∈ Word V
64 63 elexi ⊢ ⟨“ 0 1 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ Word V ∧ ⟨“ 0 2 0 3 1 2 1 2 2 3 2 3 ”⟩ ∈ 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 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
72 63 69 70 71 mp3an ⊢ ⟨“ 0 1 ”⟩ ∈ Word x ∈ 𝒫 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 ⊢ ∅ ∈ Word x ∈ 𝒫 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 ⊢ ⟨“ 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 ∈ ℕ 0
91 2le3 ⊢ 2 ≤ 3
92 elfz2nn0 ⊢ 2 ∈ 0 … 3 ↔ 2 ∈ ℕ 0 ∧ 3 ∈ ℕ 0 ∧ 2 ≤ 3
93 90 10 91 92 mpbir3an ⊢ 2 ∈ 0 … 3
94 1ne2 ⊢ 1 ≠ 2
95 94 necomi ⊢ 2 ≠ 1
96 df-s2 ⊢ ⟨“ 0 1 0 2 ”⟩ = ⟨“ 0 1 ”⟩ ++ ⟨“ 0 2 ”⟩
97 57 96 eqtri ⊢ iEdg ⁡ 0 … 3 ⟨“ 0 1 0 2 ”⟩ = ⟨“ 0 1 ”⟩ ++ ⟨“ 0 2 ”⟩
98 66 13 68 72 89 55 83 84 93 95 97 vdegp1ai ⊢ VtxDeg ⁡ 0 … 3 ⟨“ 0 1 0 2 ”⟩ ⁡ 1 = 1
99 nn0fz0 ⊢ 3 ∈ ℕ 0 ↔ 3 ∈ 0 … 3
100 10 99 mpbi ⊢ 3 ∈ 0 … 3
101 1re ⊢ 1 ∈ ℝ
102 1lt3 ⊢ 1 < 3
103 101 102 gtneii ⊢ 3 ≠ 1
104 df-s3 ⊢ ⟨“ 0 1 0 2 0 3 ”⟩ = ⟨“ 0 1 0 2 ”⟩ ++ ⟨“ 0 3 ”⟩
105 47 104 eqtri ⊢ iEdg ⁡ 0 … 3 ⟨“ 0 1 0 2 0 3 ”⟩ = ⟨“ 0 1 0 2 ”⟩ ++ ⟨“ 0 3 ”⟩
106 56 13 58 62 98 45 83 84 100 103 105 vdegp1ai ⊢ VtxDeg ⁡ 0 … 3 ⟨“ 0 1 0 2 0 3 ”⟩ ⁡ 1 = 1
107 df-s4 ⊢ ⟨“ 0 1 0 2 0 3 1 2 ”⟩ = ⟨“ 0 1 0 2 0 3 ”⟩ ++ ⟨“ 1 2 ”⟩
108 37 107 eqtri ⊢ iEdg ⁡ 0 … 3 ⟨“ 0 1 0 2 0 3 1 2 ”⟩ = ⟨“ 0 1 0 2 0 3 ”⟩ ++ ⟨“ 1 2 ”⟩
109 46 13 48 52 106 35 93 95 108 vdegp1bi ⊢ VtxDeg ⁡ 0 … 3 ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ⁡ 1 = 1 + 1
110 1p1e2 ⊢ 1 + 1 = 2
111 109 110 eqtri ⊢ VtxDeg ⁡ 0 … 3 ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ⁡ 1 = 2
112 df-s5 ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ = ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ++ ⟨“ 1 2 ”⟩
113 27 112 eqtri ⊢ iEdg ⁡ 0 … 3 ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ = ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ++ ⟨“ 1 2 ”⟩
114 36 13 38 42 111 25 93 95 113 vdegp1bi ⊢ VtxDeg ⁡ 0 … 3 ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ ⁡ 1 = 2 + 1
115 2p1e3 ⊢ 2 + 1 = 3
116 114 115 eqtri ⊢ VtxDeg ⁡ 0 … 3 ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ ⁡ 1 = 3
117 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 ”⟩
118 14 117 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 ”⟩
119 26 13 28 32 116 7 93 95 100 103 118 vdegp1ai ⊢ VtxDeg ⁡ 0 … 3 ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 ”⟩ ⁡ 1 = 3
120 1 2 3 konigsbergvtx ⊢ Vtx ⁡ G = 0 … 3
121 1 2 3 konigsbergiedg ⊢ iEdg ⁡ G = ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 2 3 ”⟩
122 121 17 eqtri ⊢ iEdg ⁡ G = ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 ”⟩ ++ ⟨“ 2 3 ”⟩
123 8 13 15 22 119 120 93 95 100 103 122 vdegp1ai ⊢ VtxDeg ⁡ G ⁡ 1 = 3