Metamath Proof Explorer

Theorem usgrexmpl2nb2

Description: The neighborhood of the third vertex of graph G . (Contributed by AV, 9-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 usgrexmpl2nb2 ⊢ G NeighbVtx 2 = 1 3

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 2ex ⊢ 2 ∈ V
5 4 tpid3 ⊢ 2 ∈ 0 1 2
6 5 orci ⊢ 2 ∈ 0 1 2 ∨ 2 ∈ 3 4 5
7 elun ⊢ 2 ∈ 0 1 2 ∪ 3 4 5 ↔ 2 ∈ 0 1 2 ∨ 2 ∈ 3 4 5
8 6 7 mpbir ⊢ 2 ∈ 0 1 2 ∪ 3 4 5
9 1 2 3 usgrexmpl2nblem ⊢ 2 ∈ 0 1 2 ∪ 3 4 5 → G NeighbVtx 2 = n ∈ 0 1 2 ∪ 3 4 5 | 2 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
10 8 9 ax-mp ⊢ G NeighbVtx 2 = n ∈ 0 1 2 ∪ 3 4 5 | 2 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
11 1eltp012 ⊢ 1 ∈ 0 1 2
12 11 orci ⊢ 1 ∈ 0 1 2 ∨ 1 ∈ 3 4 5
13 elun ⊢ 1 ∈ 0 1 2 ∪ 3 4 5 ↔ 1 ∈ 0 1 2 ∨ 1 ∈ 3 4 5
14 12 13 mpbir ⊢ 1 ∈ 0 1 2 ∪ 3 4 5
15 3ex ⊢ 3 ∈ V
16 15 tpid1 ⊢ 3 ∈ 3 4 5
17 16 olci ⊢ 3 ∈ 0 1 2 ∨ 3 ∈ 3 4 5
18 elun ⊢ 3 ∈ 0 1 2 ∪ 3 4 5 ↔ 3 ∈ 0 1 2 ∨ 3 ∈ 3 4 5
19 17 18 mpbir ⊢ 3 ∈ 0 1 2 ∪ 3 4 5
20 prssi ⊢ 1 ∈ 0 1 2 ∪ 3 4 5 ∧ 3 ∈ 0 1 2 ∪ 3 4 5 → 1 3 ⊆ 0 1 2 ∪ 3 4 5
21 vex ⊢ n ∈ V
22 4 21 pm3.2i ⊢ 2 ∈ V ∧ n ∈ V
23 c0ex ⊢ 0 ∈ V
24 1ex ⊢ 1 ∈ V
25 23 24 pm3.2i ⊢ 0 ∈ V ∧ 1 ∈ V
26 22 25 pm3.2i ⊢ 2 ∈ V ∧ n ∈ V ∧ 0 ∈ V ∧ 1 ∈ V
27 2ne0 ⊢ 2 ≠ 0
28 1ne2 ⊢ 1 ≠ 2
29 28 necomi ⊢ 2 ≠ 1
30 27 29 pm3.2i ⊢ 2 ≠ 0 ∧ 2 ≠ 1
31 30 orci ⊢ 2 ≠ 0 ∧ 2 ≠ 1 ∨ n ≠ 0 ∧ n ≠ 1
32 prneimg ⊢ 2 ∈ V ∧ n ∈ V ∧ 0 ∈ V ∧ 1 ∈ V → 2 ≠ 0 ∧ 2 ≠ 1 ∨ n ≠ 0 ∧ n ≠ 1 → 2 n ≠ 0 1
33 26 31 32 mp2 ⊢ 2 n ≠ 0 1
34 33 neii ⊢ ¬ 2 n = 0 1
35 34 biorfi ⊢ 2 n = 1 2 ∨ 2 n = 2 3 ↔ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3
36 prcom ⊢ 1 2 = 2 1
37 36 eqeq2i ⊢ 2 n = 1 2 ↔ 2 n = 2 1
38 21 a1i ⊢ 1 ∈ V → n ∈ V
39 id ⊢ 1 ∈ V → 1 ∈ V
40 38 39 preq2b ⊢ 1 ∈ V → 2 n = 2 1 ↔ n = 1
41 24 40 ax-mp ⊢ 2 n = 2 1 ↔ n = 1
42 37 41 bitr2i ⊢ n = 1 ↔ 2 n = 1 2
43 3nn0 ⊢ 3 ∈ ℕ 0
44 21 a1i ⊢ 3 ∈ ℕ 0 → n ∈ V
45 id ⊢ 3 ∈ ℕ 0 → 3 ∈ ℕ 0
46 44 45 preq2b ⊢ 3 ∈ ℕ 0 → 2 n = 2 3 ↔ n = 3
47 46 bicomd ⊢ 3 ∈ ℕ 0 → n = 3 ↔ 2 n = 2 3
48 43 47 ax-mp ⊢ n = 3 ↔ 2 n = 2 3
49 42 48 orbi12i ⊢ n = 1 ∨ n = 3 ↔ 2 n = 1 2 ∨ 2 n = 2 3
50 3orass ⊢ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3 ↔ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3
51 35 49 50 3bitr4i ⊢ n = 1 ∨ n = 3 ↔ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3
52 2re ⊢ 2 ∈ ℝ
53 52 21 pm3.2i ⊢ 2 ∈ ℝ ∧ n ∈ V
54 4nn0 ⊢ 4 ∈ ℕ 0
55 15 54 pm3.2i ⊢ 3 ∈ V ∧ 4 ∈ ℕ 0
56 53 55 pm3.2i ⊢ 2 ∈ ℝ ∧ n ∈ V ∧ 3 ∈ V ∧ 4 ∈ ℕ 0
57 2lt3 ⊢ 2 < 3
58 52 57 ltneii ⊢ 2 ≠ 3
59 2lt4 ⊢ 2 < 4
60 52 59 ltneii ⊢ 2 ≠ 4
61 58 60 pm3.2i ⊢ 2 ≠ 3 ∧ 2 ≠ 4
62 61 orci ⊢ 2 ≠ 3 ∧ 2 ≠ 4 ∨ n ≠ 3 ∧ n ≠ 4
63 prneimg ⊢ 2 ∈ ℝ ∧ n ∈ V ∧ 3 ∈ V ∧ 4 ∈ ℕ 0 → 2 ≠ 3 ∧ 2 ≠ 4 ∨ n ≠ 3 ∧ n ≠ 4 → 2 n ≠ 3 4
64 56 62 63 mp2 ⊢ 2 n ≠ 3 4
65 64 neii ⊢ ¬ 2 n = 3 4
66 5nn0 ⊢ 5 ∈ ℕ 0
67 54 66 pm3.2i ⊢ 4 ∈ ℕ 0 ∧ 5 ∈ ℕ 0
68 53 67 pm3.2i ⊢ 2 ∈ ℝ ∧ n ∈ V ∧ 4 ∈ ℕ 0 ∧ 5 ∈ ℕ 0
69 2lt5 ⊢ 2 < 5
70 52 69 ltneii ⊢ 2 ≠ 5
71 60 70 pm3.2i ⊢ 2 ≠ 4 ∧ 2 ≠ 5
72 71 orci ⊢ 2 ≠ 4 ∧ 2 ≠ 5 ∨ n ≠ 4 ∧ n ≠ 5
73 prneimg ⊢ 2 ∈ ℝ ∧ n ∈ V ∧ 4 ∈ ℕ 0 ∧ 5 ∈ ℕ 0 → 2 ≠ 4 ∧ 2 ≠ 5 ∨ n ≠ 4 ∧ n ≠ 5 → 2 n ≠ 4 5
74 68 72 73 mp2 ⊢ 2 n ≠ 4 5
75 74 neii ⊢ ¬ 2 n = 4 5
76 23 66 pm3.2i ⊢ 0 ∈ V ∧ 5 ∈ ℕ 0
77 53 76 pm3.2i ⊢ 2 ∈ ℝ ∧ n ∈ V ∧ 0 ∈ V ∧ 5 ∈ ℕ 0
78 27 70 pm3.2i ⊢ 2 ≠ 0 ∧ 2 ≠ 5
79 78 orci ⊢ 2 ≠ 0 ∧ 2 ≠ 5 ∨ n ≠ 0 ∧ n ≠ 5
80 prneimg ⊢ 2 ∈ ℝ ∧ n ∈ V ∧ 0 ∈ V ∧ 5 ∈ ℕ 0 → 2 ≠ 0 ∧ 2 ≠ 5 ∨ n ≠ 0 ∧ n ≠ 5 → 2 n ≠ 0 5
81 77 79 80 mp2 ⊢ 2 n ≠ 0 5
82 81 neii ⊢ ¬ 2 n = 0 5
83 65 75 82 3pm3.2ni ⊢ ¬ 2 n = 3 4 ∨ 2 n = 4 5 ∨ 2 n = 0 5
84 83 biorfri ⊢ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3 ↔ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3 ∨ 2 n = 3 4 ∨ 2 n = 4 5 ∨ 2 n = 0 5
85 23 15 pm3.2i ⊢ 0 ∈ V ∧ 3 ∈ V
86 53 85 pm3.2i ⊢ 2 ∈ ℝ ∧ n ∈ V ∧ 0 ∈ V ∧ 3 ∈ V
87 27 58 pm3.2i ⊢ 2 ≠ 0 ∧ 2 ≠ 3
88 87 orci ⊢ 2 ≠ 0 ∧ 2 ≠ 3 ∨ n ≠ 0 ∧ n ≠ 3
89 prneimg ⊢ 2 ∈ ℝ ∧ n ∈ V ∧ 0 ∈ V ∧ 3 ∈ V → 2 ≠ 0 ∧ 2 ≠ 3 ∨ n ≠ 0 ∧ n ≠ 3 → 2 n ≠ 0 3
90 86 88 89 mp2 ⊢ 2 n ≠ 0 3
91 90 neii ⊢ ¬ 2 n = 0 3
92 91 biorfi ⊢ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3 ∨ 2 n = 3 4 ∨ 2 n = 4 5 ∨ 2 n = 0 5 ↔ 2 n = 0 3 ∨ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3 ∨ 2 n = 3 4 ∨ 2 n = 4 5 ∨ 2 n = 0 5
93 51 84 92 3bitri ⊢ n = 1 ∨ n = 3 ↔ 2 n = 0 3 ∨ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3 ∨ 2 n = 3 4 ∨ 2 n = 4 5 ∨ 2 n = 0 5
94 21 elpr ⊢ n ∈ 1 3 ↔ n = 1 ∨ n = 3
95 prex ⊢ 2 n ∈ V
96 el7g ⊢ 2 n ∈ V → 2 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ 2 n = 0 3 ∨ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3 ∨ 2 n = 3 4 ∨ 2 n = 4 5 ∨ 2 n = 0 5
97 95 96 ax-mp ⊢ 2 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ 2 n = 0 3 ∨ 2 n = 0 1 ∨ 2 n = 1 2 ∨ 2 n = 2 3 ∨ 2 n = 3 4 ∨ 2 n = 4 5 ∨ 2 n = 0 5
98 93 94 97 3bitr4i ⊢ n ∈ 1 3 ↔ 2 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
99 98 a1i ⊢ 1 ∈ 0 1 2 ∪ 3 4 5 ∧ 3 ∈ 0 1 2 ∪ 3 4 5 ∧ n ∈ 0 1 2 ∪ 3 4 5 → n ∈ 1 3 ↔ 2 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
100 20 99 eqrrabd ⊢ 1 ∈ 0 1 2 ∪ 3 4 5 ∧ 3 ∈ 0 1 2 ∪ 3 4 5 → 1 3 = n ∈ 0 1 2 ∪ 3 4 5 | 2 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
101 100 eqcomd ⊢ 1 ∈ 0 1 2 ∪ 3 4 5 ∧ 3 ∈ 0 1 2 ∪ 3 4 5 → n ∈ 0 1 2 ∪ 3 4 5 | 2 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 = 1 3
102 14 19 101 mp2an ⊢ n ∈ 0 1 2 ∪ 3 4 5 | 2 n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 = 1 3
103 10 102 eqtri ⊢ G NeighbVtx 2 = 1 3