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