Metamath Proof Explorer

Theorem usgrexmpl2nb3

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