Metamath Proof Explorer

Theorem usgrexmpl2nb5

Description: The neighborhood of the sixth vertex of graph G . (Contributed by AV, 10-Aug-2025)

Ref Expression
Hypotheses usgrexmpl2.v ⊢ V = 0 … 5
usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
usgrexmpl2.g ⊢ G = V E
Assertion usgrexmpl2nb5 ⊢ G NeighbVtx 5 = 0 4

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ V = 0 … 5
2 usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
3 usgrexmpl2.g ⊢ G = V E
4 5re ⊢ 5 ∈ ℝ
5 4 elexi ⊢ 5 ∈ V
6 5 tpid3 ⊢ 5 ∈ 3 4 5
7 6 olci ⊢ 5 ∈ 0 1 2 ∨ 5 ∈ 3 4 5
8 elun ⊢ 5 ∈ 0 1 2 ∪ 3 4 5 ↔ 5 ∈ 0 1 2 ∨ 5 ∈ 3 4 5
9 7 8 mpbir ⊢ 5 ∈ 0 1 2 ∪ 3 4 5
10 1 2 3 usgrexmpl2nblem ⊢ 5 ∈ 0 1 2 ∪ 3 4 5 → G NeighbVtx 5 = n ∈ 0 1 2 ∪ 3 4 5 | 5 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
11 9 10 ax-mp ⊢ G NeighbVtx 5 = n ∈ 0 1 2 ∪ 3 4 5 | 5 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
12 c0ex ⊢ 0 ∈ V
13 12 tpid1 ⊢ 0 ∈ 0 1 2
14 13 orci ⊢ 0 ∈ 0 1 2 ∨ 0 ∈ 3 4 5
15 elun ⊢ 0 ∈ 0 1 2 ∪ 3 4 5 ↔ 0 ∈ 0 1 2 ∨ 0 ∈ 3 4 5
16 14 15 mpbir ⊢ 0 ∈ 0 1 2 ∪ 3 4 5
17 4re ⊢ 4 ∈ ℝ
18 17 elexi ⊢ 4 ∈ V
19 18 tpid2 ⊢ 4 ∈ 3 4 5
20 19 olci ⊢ 4 ∈ 0 1 2 ∨ 4 ∈ 3 4 5
21 elun ⊢ 4 ∈ 0 1 2 ∪ 3 4 5 ↔ 4 ∈ 0 1 2 ∨ 4 ∈ 3 4 5
22 20 21 mpbir ⊢ 4 ∈ 0 1 2 ∪ 3 4 5
23 prssi ⊢ 0 ∈ 0 1 2 ∪ 3 4 5 ∧ 4 ∈ 0 1 2 ∪ 3 4 5 → 0 4 ⊆ 0 1 2 ∪ 3 4 5
24 vex ⊢ n ∈ V
25 4 24 pm3.2i ⊢ 5 ∈ ℝ ∧ n ∈ V
26 3re ⊢ 3 ∈ ℝ
27 26 17 pm3.2i ⊢ 3 ∈ ℝ ∧ 4 ∈ ℝ
28 25 27 pm3.2i ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 3 ∈ ℝ ∧ 4 ∈ ℝ
29 3lt5 ⊢ 3 < 5
30 26 29 gtneii ⊢ 5 ≠ 3
31 4lt5 ⊢ 4 < 5
32 17 31 gtneii ⊢ 5 ≠ 4
33 30 32 pm3.2i ⊢ 5 ≠ 3 ∧ 5 ≠ 4
34 33 orci ⊢ 5 ≠ 3 ∧ 5 ≠ 4 ∨ n ≠ 3 ∧ n ≠ 4
35 prneimg ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 3 ∈ ℝ ∧ 4 ∈ ℝ → 5 ≠ 3 ∧ 5 ≠ 4 ∨ n ≠ 3 ∧ n ≠ 4 → 5 n ≠ 3 4
36 28 34 35 mp2 ⊢ 5 n ≠ 3 4
37 36 neii ⊢ ¬ 5 n = 3 4
38 37 biorfi ⊢ 5 n = 4 5 ∨ 5 n = 0 5 ↔ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5
39 orcom ⊢ n = 0 ∨ n = 4 ↔ n = 4 ∨ n = 0
40 prcom ⊢ 4 5 = 5 4
41 40 eqeq2i ⊢ 5 n = 4 5 ↔ 5 n = 5 4
42 24 a1i ⊢ 4 ∈ ℝ → n ∈ V
43 id ⊢ 4 ∈ ℝ → 4 ∈ ℝ
44 42 43 preq2b ⊢ 4 ∈ ℝ → 5 n = 5 4 ↔ n = 4
45 17 44 ax-mp ⊢ 5 n = 5 4 ↔ n = 4
46 41 45 bitr2i ⊢ n = 4 ↔ 5 n = 4 5
47 prcom ⊢ 0 5 = 5 0
48 47 eqeq2i ⊢ 5 n = 0 5 ↔ 5 n = 5 0
49 24 a1i ⊢ 0 ∈ V → n ∈ V
50 id ⊢ 0 ∈ V → 0 ∈ V
51 49 50 preq2b ⊢ 0 ∈ V → 5 n = 5 0 ↔ n = 0
52 12 51 ax-mp ⊢ 5 n = 5 0 ↔ n = 0
53 48 52 bitr2i ⊢ n = 0 ↔ 5 n = 0 5
54 46 53 orbi12i ⊢ n = 4 ∨ n = 0 ↔ 5 n = 4 5 ∨ 5 n = 0 5
55 39 54 bitri ⊢ n = 0 ∨ n = 4 ↔ 5 n = 4 5 ∨ 5 n = 0 5
56 3orass ⊢ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5 ↔ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5
57 38 55 56 3bitr4i ⊢ n = 0 ∨ n = 4 ↔ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5
58 0re ⊢ 0 ∈ ℝ
59 1re ⊢ 1 ∈ ℝ
60 58 59 pm3.2i ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ
61 25 60 pm3.2i ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ
62 5pos ⊢ 0 < 5
63 58 62 gtneii ⊢ 5 ≠ 0
64 1lt5 ⊢ 1 < 5
65 59 64 gtneii ⊢ 5 ≠ 1
66 63 65 pm3.2i ⊢ 5 ≠ 0 ∧ 5 ≠ 1
67 66 orci ⊢ 5 ≠ 0 ∧ 5 ≠ 1 ∨ n ≠ 0 ∧ n ≠ 1
68 prneimg ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ → 5 ≠ 0 ∧ 5 ≠ 1 ∨ n ≠ 0 ∧ n ≠ 1 → 5 n ≠ 0 1
69 61 67 68 mp2 ⊢ 5 n ≠ 0 1
70 69 neii ⊢ ¬ 5 n = 0 1
71 2re ⊢ 2 ∈ ℝ
72 59 71 pm3.2i ⊢ 1 ∈ ℝ ∧ 2 ∈ ℝ
73 25 72 pm3.2i ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 1 ∈ ℝ ∧ 2 ∈ ℝ
74 2lt5 ⊢ 2 < 5
75 71 74 gtneii ⊢ 5 ≠ 2
76 65 75 pm3.2i ⊢ 5 ≠ 1 ∧ 5 ≠ 2
77 76 orci ⊢ 5 ≠ 1 ∧ 5 ≠ 2 ∨ n ≠ 1 ∧ n ≠ 2
78 prneimg ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 1 ∈ ℝ ∧ 2 ∈ ℝ → 5 ≠ 1 ∧ 5 ≠ 2 ∨ n ≠ 1 ∧ n ≠ 2 → 5 n ≠ 1 2
79 73 77 78 mp2 ⊢ 5 n ≠ 1 2
80 79 neii ⊢ ¬ 5 n = 1 2
81 71 26 pm3.2i ⊢ 2 ∈ ℝ ∧ 3 ∈ ℝ
82 25 81 pm3.2i ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 2 ∈ ℝ ∧ 3 ∈ ℝ
83 75 30 pm3.2i ⊢ 5 ≠ 2 ∧ 5 ≠ 3
84 83 orci ⊢ 5 ≠ 2 ∧ 5 ≠ 3 ∨ n ≠ 2 ∧ n ≠ 3
85 prneimg ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 2 ∈ ℝ ∧ 3 ∈ ℝ → 5 ≠ 2 ∧ 5 ≠ 3 ∨ n ≠ 2 ∧ n ≠ 3 → 5 n ≠ 2 3
86 82 84 85 mp2 ⊢ 5 n ≠ 2 3
87 86 neii ⊢ ¬ 5 n = 2 3
88 70 80 87 3pm3.2ni ⊢ ¬ 5 n = 0 1 ∨ 5 n = 1 2 ∨ 5 n = 2 3
89 88 biorfi ⊢ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5 ↔ 5 n = 0 1 ∨ 5 n = 1 2 ∨ 5 n = 2 3 ∨ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5
90 57 89 bitri ⊢ n = 0 ∨ n = 4 ↔ 5 n = 0 1 ∨ 5 n = 1 2 ∨ 5 n = 2 3 ∨ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5
91 58 26 pm3.2i ⊢ 0 ∈ ℝ ∧ 3 ∈ ℝ
92 25 91 pm3.2i ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 0 ∈ ℝ ∧ 3 ∈ ℝ
93 63 30 pm3.2i ⊢ 5 ≠ 0 ∧ 5 ≠ 3
94 93 orci ⊢ 5 ≠ 0 ∧ 5 ≠ 3 ∨ n ≠ 0 ∧ n ≠ 3
95 prneimg ⊢ 5 ∈ ℝ ∧ n ∈ V ∧ 0 ∈ ℝ ∧ 3 ∈ ℝ → 5 ≠ 0 ∧ 5 ≠ 3 ∨ n ≠ 0 ∧ n ≠ 3 → 5 n ≠ 0 3
96 92 94 95 mp2 ⊢ 5 n ≠ 0 3
97 96 neii ⊢ ¬ 5 n = 0 3
98 97 biorfi ⊢ 5 n = 0 1 ∨ 5 n = 1 2 ∨ 5 n = 2 3 ∨ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5 ↔ 5 n = 0 3 ∨ 5 n = 0 1 ∨ 5 n = 1 2 ∨ 5 n = 2 3 ∨ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5
99 90 98 bitri ⊢ n = 0 ∨ n = 4 ↔ 5 n = 0 3 ∨ 5 n = 0 1 ∨ 5 n = 1 2 ∨ 5 n = 2 3 ∨ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5
100 24 elpr ⊢ n ∈ 0 4 ↔ n = 0 ∨ n = 4
101 prex ⊢ 5 n ∈ V
102 el7g ⊢ 5 n ∈ V → 5 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ 5 n = 0 3 ∨ 5 n = 0 1 ∨ 5 n = 1 2 ∨ 5 n = 2 3 ∨ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5
103 101 102 ax-mp ⊢ 5 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ 5 n = 0 3 ∨ 5 n = 0 1 ∨ 5 n = 1 2 ∨ 5 n = 2 3 ∨ 5 n = 3 4 ∨ 5 n = 4 5 ∨ 5 n = 0 5
104 99 100 103 3bitr4i ⊢ n ∈ 0 4 ↔ 5 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
105 104 a1i ⊢ 0 ∈ 0 1 2 ∪ 3 4 5 ∧ 4 ∈ 0 1 2 ∪ 3 4 5 ∧ n ∈ 0 1 2 ∪ 3 4 5 → n ∈ 0 4 ↔ 5 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
106 23 105 eqrrabd ⊢ 0 ∈ 0 1 2 ∪ 3 4 5 ∧ 4 ∈ 0 1 2 ∪ 3 4 5 → 0 4 = n ∈ 0 1 2 ∪ 3 4 5 | 5 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
107 106 eqcomd ⊢ 0 ∈ 0 1 2 ∪ 3 4 5 ∧ 4 ∈ 0 1 2 ∪ 3 4 5 → n ∈ 0 1 2 ∪ 3 4 5 | 5 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 = 0 4
108 16 22 107 mp2an ⊢ n ∈ 0 1 2 ∪ 3 4 5 | 5 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 = 0 4
109 11 108 eqtri ⊢ G NeighbVtx 5 = 0 4