Metamath Proof Explorer

Theorem usgrexmpl2nb4

Description: The neighborhood of the fifth 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 usgrexmpl2nb4 ⊢ G NeighbVtx 4 = 3 5

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