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 ∈ 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 3nn0 ⊢ 3 ∈ ℕ 0
10 nn0fz0 ⊢ 3 ∈ ℕ 0 ↔ 3 ∈ 0 … 3
11 9 10 mpbi ⊢ 3 ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ 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
20 5 14 15 19 mp3an ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
21 s5cli ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ ∈ Word V
22 21 elexi ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ 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
30 21 27 28 29 mp3an ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
31 s4cli ⊢ ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ∈ Word V
32 31 elexi ⊢ ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ 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
40 31 37 38 39 mp3an ⊢ ⟨“ 0 1 0 2 0 3 1 2 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
41 s3cli ⊢ ⟨“ 0 1 0 2 0 3 ”⟩ ∈ Word V
42 41 elexi ⊢ ⟨“ 0 1 0 2 0 3 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ 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
50 41 47 48 49 mp3an ⊢ ⟨“ 0 1 0 2 0 3 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
51 s2cli ⊢ ⟨“ 0 1 0 2 ”⟩ ∈ Word V
52 51 elexi ⊢ ⟨“ 0 1 0 2 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ 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
60 51 57 58 59 mp3an ⊢ ⟨“ 0 1 0 2 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 ∖ ∅ | x ≤ 2
61 s1cli ⊢ ⟨“ 0 1 ”⟩ ∈ Word V
62 61 elexi ⊢ ⟨“ 0 1 ”⟩ ∈ 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 ”⟩ ∈ 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 ”⟩ ∈ 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
70 61 67 68 69 mp3an ⊢ ⟨“ 0 1 ”⟩ ∈ Word x ∈ 𝒫 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 ⊢ ∅ ∈ Word x ∈ 𝒫 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 ⊢ ⟨“ 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 ∈ ℕ 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 ⊢ ⟨“ 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