Metamath Proof Explorer


Theorem usgrexmpl2nb2

Description: The neighborhood of the third 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 usgrexmpl2nb2 G NeighbVtx 2 = 1 3

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