Metamath Proof Explorer


Theorem usgrexmpl2nb4

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