Metamath Proof Explorer

Theorem usgrexmpl2nb0

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