Metamath Proof Explorer

Theorem usgrexmpl2nb1

Description: The neighborhood of the second 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 usgrexmpl2nb1 ⊢ G NeighbVtx 1 = 0 2

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