Metamath Proof Explorer


Theorem usgrexmpl2nb3

Description: The neighborhood of the forth 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 usgrexmpl2nb3 G NeighbVtx 3 = 0 2 4

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 3ex 3 V
5 4 tpid1 3 3 4 5
6 5 olci 3 0 1 2 3 3 4 5
7 elun 3 0 1 2 3 4 5 3 0 1 2 3 3 4 5
8 6 7 mpbir 3 0 1 2 3 4 5
9 1 2 3 usgrexmpl2nblem 3 0 1 2 3 4 5 G NeighbVtx 3 = n 0 1 2 3 4 5 | 3 n 0 3 0 1 1 2 2 3 3 4 4 5 0 5
10 8 9 ax-mp G NeighbVtx 3 = n 0 1 2 3 4 5 | 3 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 4nn0 4 0
22 21 elexi 4 V
23 22 tpid2 4 3 4 5
24 23 olci 4 0 1 2 4 3 4 5
25 elun 4 0 1 2 3 4 5 4 0 1 2 4 3 4 5
26 24 25 mpbir 4 0 1 2 3 4 5
27 tpssi 0 0 1 2 3 4 5 2 0 1 2 3 4 5 4 0 1 2 3 4 5 0 2 4 0 1 2 3 4 5
28 3orass n = 0 n = 2 n = 4 n = 0 n = 2 n = 4
29 vex n V
30 29 eltp n 0 2 4 n = 0 n = 2 n = 4
31 prex 3 n V
32 el7g 3 n V 3 n 0 3 0 1 1 2 2 3 3 4 4 5 0 5 3 n = 0 3 3 n = 0 1 3 n = 1 2 3 n = 2 3 3 n = 3 4 3 n = 4 5 3 n = 0 5
33 31 32 ax-mp 3 n 0 3 0 1 1 2 2 3 3 4 4 5 0 5 3 n = 0 3 3 n = 0 1 3 n = 1 2 3 n = 2 3 3 n = 3 4 3 n = 4 5 3 n = 0 5
34 prcom 0 3 = 3 0
35 34 eqeq2i 3 n = 0 3 3 n = 3 0
36 29 a1i 0 V n V
37 elex 0 V 0 V
38 36 37 preq2b 0 V 3 n = 3 0 n = 0
39 11 38 ax-mp 3 n = 3 0 n = 0
40 35 39 bitri 3 n = 0 3 n = 0
41 3orrot 3 n = 0 1 3 n = 1 2 3 n = 2 3 3 n = 1 2 3 n = 2 3 3 n = 0 1
42 4 29 pm3.2i 3 V n V
43 1re 1
44 43 16 pm3.2i 1 2 V
45 42 44 pm3.2i 3 V n V 1 2 V
46 1lt3 1 < 3
47 43 46 gtneii 3 1
48 2re 2
49 2lt3 2 < 3
50 48 49 gtneii 3 2
51 47 50 pm3.2i 3 1 3 2
52 51 orci 3 1 3 2 n 1 n 2
53 prneimg 3 V n V 1 2 V 3 1 3 2 n 1 n 2 3 n 1 2
54 45 52 53 mp2 3 n 1 2
55 54 neii ¬ 3 n = 1 2
56 id ¬ 3 n = 1 2 ¬ 3 n = 1 2
57 11 43 pm3.2i 0 V 1
58 42 57 pm3.2i 3 V n V 0 V 1
59 3ne0 3 0
60 59 47 pm3.2i 3 0 3 1
61 60 orci 3 0 3 1 n 0 n 1
62 prneimg 3 V n V 0 V 1 3 0 3 1 n 0 n 1 3 n 0 1
63 58 61 62 mp2 3 n 0 1
64 63 neii ¬ 3 n = 0 1
65 64 a1i ¬ 3 n = 1 2 ¬ 3 n = 0 1
66 56 65 3bior2fd ¬ 3 n = 1 2 3 n = 2 3 3 n = 1 2 3 n = 0 1 3 n = 2 3
67 55 66 ax-mp 3 n = 2 3 3 n = 1 2 3 n = 0 1 3 n = 2 3
68 3orcomb 3 n = 1 2 3 n = 0 1 3 n = 2 3 3 n = 1 2 3 n = 2 3 3 n = 0 1
69 67 68 bitri 3 n = 2 3 3 n = 1 2 3 n = 2 3 3 n = 0 1
70 prcom 2 3 = 3 2
71 70 eqeq2i 3 n = 2 3 3 n = 3 2
72 29 a1i 2 V n V
73 elex 2 V 2 V
74 72 73 preq2b 2 V 3 n = 3 2 n = 2
75 16 74 ax-mp 3 n = 3 2 n = 2
76 71 75 bitri 3 n = 2 3 n = 2
77 41 69 76 3bitr2i 3 n = 0 1 3 n = 1 2 3 n = 2 3 n = 2
78 3orrot 3 n = 3 4 3 n = 4 5 3 n = 0 5 3 n = 4 5 3 n = 0 5 3 n = 3 4
79 5nn0 5 0
80 21 79 pm3.2i 4 0 5 0
81 42 80 pm3.2i 3 V n V 4 0 5 0
82 3re 3
83 3lt4 3 < 4
84 82 83 ltneii 3 4
85 3lt5 3 < 5
86 82 85 ltneii 3 5
87 84 86 pm3.2i 3 4 3 5
88 87 orci 3 4 3 5 n 4 n 5
89 prneimg 3 V n V 4 0 5 0 3 4 3 5 n 4 n 5 3 n 4 5
90 81 88 89 mp2 3 n 4 5
91 90 neii ¬ 3 n = 4 5
92 id ¬ 3 n = 4 5 ¬ 3 n = 4 5
93 11 79 pm3.2i 0 V 5 0
94 42 93 pm3.2i 3 V n V 0 V 5 0
95 59 86 pm3.2i 3 0 3 5
96 95 orci 3 0 3 5 n 0 n 5
97 prneimg 3 V n V 0 V 5 0 3 0 3 5 n 0 n 5 3 n 0 5
98 94 96 97 mp2 3 n 0 5
99 98 neii ¬ 3 n = 0 5
100 99 a1i ¬ 3 n = 4 5 ¬ 3 n = 0 5
101 92 100 3bior2fd ¬ 3 n = 4 5 3 n = 3 4 3 n = 4 5 3 n = 0 5 3 n = 3 4
102 91 101 ax-mp 3 n = 3 4 3 n = 4 5 3 n = 0 5 3 n = 3 4
103 29 a1i 4 0 n V
104 elex 4 0 4 V
105 103 104 preq2b 4 0 3 n = 3 4 n = 4
106 21 105 ax-mp 3 n = 3 4 n = 4
107 78 102 106 3bitr2i 3 n = 3 4 3 n = 4 5 3 n = 0 5 n = 4
108 77 107 orbi12i 3 n = 0 1 3 n = 1 2 3 n = 2 3 3 n = 3 4 3 n = 4 5 3 n = 0 5 n = 2 n = 4
109 40 108 orbi12i 3 n = 0 3 3 n = 0 1 3 n = 1 2 3 n = 2 3 3 n = 3 4 3 n = 4 5 3 n = 0 5 n = 0 n = 2 n = 4
110 33 109 bitri 3 n 0 3 0 1 1 2 2 3 3 4 4 5 0 5 n = 0 n = 2 n = 4
111 28 30 110 3bitr4i n 0 2 4 3 n 0 3 0 1 1 2 2 3 3 4 4 5 0 5
112 111 a1i 0 0 1 2 3 4 5 2 0 1 2 3 4 5 4 0 1 2 3 4 5 n 0 1 2 3 4 5 n 0 2 4 3 n 0 3 0 1 1 2 2 3 3 4 4 5 0 5
113 27 112 eqrrabd 0 0 1 2 3 4 5 2 0 1 2 3 4 5 4 0 1 2 3 4 5 0 2 4 = n 0 1 2 3 4 5 | 3 n 0 3 0 1 1 2 2 3 3 4 4 5 0 5
114 15 20 26 113 mp3an 0 2 4 = n 0 1 2 3 4 5 | 3 n 0 3 0 1 1 2 2 3 3 4 4 5 0 5
115 10 114 eqtr4i G NeighbVtx 3 = 0 2 4