Metamath Proof Explorer

Theorem konigsbergiedgw

Description: The indexed edges of the Königsberg graph G is a word over the pairs of vertices. (Contributed by AV, 28-Feb-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 konigsbergiedgw ⊢ E ∈ Word x ∈ 𝒫 V | x = 2

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 3nn0 ⊢ 3 ∈ ℕ 0
5 0elfz ⊢ 3 ∈ ℕ 0 → 0 ∈ 0 … 3
6 4 5 ax-mp ⊢ 0 ∈ 0 … 3
7 1nn0 ⊢ 1 ∈ ℕ 0
8 1le3 ⊢ 1 ≤ 3
9 elfz2nn0 ⊢ 1 ∈ 0 … 3 ↔ 1 ∈ ℕ 0 ∧ 3 ∈ ℕ 0 ∧ 1 ≤ 3
10 7 4 8 9 mpbir3an ⊢ 1 ∈ 0 … 3
11 0ne1 ⊢ 0 ≠ 1
12 6 10 11 umgrbi ⊢ 0 1 ∈ x ∈ 𝒫 0 … 3 | x = 2
13 12 a1i ⊢ ⊤ → 0 1 ∈ x ∈ 𝒫 0 … 3 | x = 2
14 2nn0 ⊢ 2 ∈ ℕ 0
15 2re ⊢ 2 ∈ ℝ
16 3re ⊢ 3 ∈ ℝ
17 2lt3 ⊢ 2 < 3
18 15 16 17 ltleii ⊢ 2 ≤ 3
19 elfz2nn0 ⊢ 2 ∈ 0 … 3 ↔ 2 ∈ ℕ 0 ∧ 3 ∈ ℕ 0 ∧ 2 ≤ 3
20 14 4 18 19 mpbir3an ⊢ 2 ∈ 0 … 3
21 0ne2 ⊢ 0 ≠ 2
22 6 20 21 umgrbi ⊢ 0 2 ∈ x ∈ 𝒫 0 … 3 | x = 2
23 22 a1i ⊢ ⊤ → 0 2 ∈ x ∈ 𝒫 0 … 3 | x = 2
24 nn0fz0 ⊢ 3 ∈ ℕ 0 ↔ 3 ∈ 0 … 3
25 4 24 mpbi ⊢ 3 ∈ 0 … 3
26 3ne0 ⊢ 3 ≠ 0
27 26 necomi ⊢ 0 ≠ 3
28 6 25 27 umgrbi ⊢ 0 3 ∈ x ∈ 𝒫 0 … 3 | x = 2
29 28 a1i ⊢ ⊤ → 0 3 ∈ x ∈ 𝒫 0 … 3 | x = 2
30 1ne2 ⊢ 1 ≠ 2
31 10 20 30 umgrbi ⊢ 1 2 ∈ x ∈ 𝒫 0 … 3 | x = 2
32 31 a1i ⊢ ⊤ → 1 2 ∈ x ∈ 𝒫 0 … 3 | x = 2
33 15 17 ltneii ⊢ 2 ≠ 3
34 20 25 33 umgrbi ⊢ 2 3 ∈ x ∈ 𝒫 0 … 3 | x = 2
35 34 a1i ⊢ ⊤ → 2 3 ∈ x ∈ 𝒫 0 … 3 | x = 2
36 13 23 29 32 32 35 35 s7cld ⊢ ⊤ → ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 2 3 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 | x = 2
37 36 mptru ⊢ ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 2 3 ”⟩ ∈ Word x ∈ 𝒫 0 … 3 | x = 2
38 1 pweqi ⊢ 𝒫 V = 𝒫 0 … 3
39 38 rabeqi ⊢ x ∈ 𝒫 V | x = 2 = x ∈ 𝒫 0 … 3 | x = 2
40 39 wrdeqi ⊢ Word x ∈ 𝒫 V | x = 2 = Word x ∈ 𝒫 0 … 3 | x = 2
41 37 2 40 3eltr4i ⊢ E ∈ Word x ∈ 𝒫 V | x = 2