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 e. _V
5 4 tpid1 
 |-  0 e. { 0 , 1 , 2 }
6 5 orci 
 |-  ( 0 e. { 0 , 1 , 2 } \/ 0 e. { 3 , 4 , 5 } )
7 elun 
 |-  ( 0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 0 e. { 0 , 1 , 2 } \/ 0 e. { 3 , 4 , 5 } ) )
8 6 7 mpbir 
 |-  0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
9 1 2 3 usgrexmpl2nblem 
 |-  ( 0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) -> ( G NeighbVtx 0 ) = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { 0 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )
10 8 9 ax-mp 
 |-  ( G NeighbVtx 0 ) = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { 0 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) }
11 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
12 11 orci 
 |-  ( 1 e. { 0 , 1 , 2 } \/ 1 e. { 3 , 4 , 5 } )
13 elun 
 |-  ( 1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 1 e. { 0 , 1 , 2 } \/ 1 e. { 3 , 4 , 5 } ) )
14 12 13 mpbir 
 |-  1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
15 3ex 
 |-  3 e. _V
16 15 tpid1 
 |-  3 e. { 3 , 4 , 5 }
17 16 olci 
 |-  ( 3 e. { 0 , 1 , 2 } \/ 3 e. { 3 , 4 , 5 } )
18 elun 
 |-  ( 3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 3 e. { 0 , 1 , 2 } \/ 3 e. { 3 , 4 , 5 } ) )
19 17 18 mpbir 
 |-  3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
20 5nn0 
 |-  5 e. NN0
21 20 elexi 
 |-  5 e. _V
22 21 tpid3 
 |-  5 e. { 3 , 4 , 5 }
23 22 olci 
 |-  ( 5 e. { 0 , 1 , 2 } \/ 5 e. { 3 , 4 , 5 } )
24 elun 
 |-  ( 5 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 5 e. { 0 , 1 , 2 } \/ 5 e. { 3 , 4 , 5 } ) )
25 23 24 mpbir 
 |-  5 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
26 tpssi 
 |-  ( ( 1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 5 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) -> { 1 , 3 , 5 } C_ ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) )
27 3orcoma 
 |-  ( ( n = 3 \/ n = 1 \/ n = 5 ) <-> ( n = 1 \/ n = 3 \/ n = 5 ) )
28 3orass 
 |-  ( ( n = 3 \/ n = 1 \/ n = 5 ) <-> ( n = 3 \/ ( n = 1 \/ n = 5 ) ) )
29 27 28 bitr3i 
 |-  ( ( n = 1 \/ n = 3 \/ n = 5 ) <-> ( n = 3 \/ ( n = 1 \/ n = 5 ) ) )
30 vex 
 |-  n e. _V
31 30 eltp 
 |-  ( n e. { 1 , 3 , 5 } <-> ( n = 1 \/ n = 3 \/ n = 5 ) )
32 prex 
 |-  { 0 , n } e. _V
33 el7g 
 |-  ( { 0 , n } e. _V -> ( { 0 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 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 } ) ) ) ) )
34 32 33 ax-mp 
 |-  ( { 0 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 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 30 a1i 
 |-  ( 3 e. _V -> n e. _V )
36 elex 
 |-  ( 3 e. _V -> 3 e. _V )
37 35 36 preq2b 
 |-  ( 3 e. _V -> ( { 0 , n } = { 0 , 3 } <-> n = 3 ) )
38 15 37 ax-mp 
 |-  ( { 0 , n } = { 0 , 3 } <-> n = 3 )
39 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 } ) )
40 4 30 pm3.2i 
 |-  ( 0 e. _V /\ n e. _V )
41 1ex 
 |-  1 e. _V
42 2ex 
 |-  2 e. _V
43 41 42 pm3.2i 
 |-  ( 1 e. _V /\ 2 e. _V )
44 40 43 pm3.2i 
 |-  ( ( 0 e. _V /\ n e. _V ) /\ ( 1 e. _V /\ 2 e. _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 e. _V /\ n e. _V ) /\ ( 1 e. _V /\ 2 e. _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 15 pm3.2i 
 |-  ( 2 e. _V /\ 3 e. _V )
54 40 53 pm3.2i 
 |-  ( ( 0 e. _V /\ n e. _V ) /\ ( 2 e. _V /\ 3 e. _V ) )
55 0re 
 |-  0 e. RR
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 e. _V /\ n e. _V ) /\ ( 2 e. _V /\ 3 e. _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 30 a1i 
 |-  ( 1 e. _V -> n e. _V )
67 elex 
 |-  ( 1 e. _V -> 1 e. _V )
68 66 67 preq2b 
 |-  ( 1 e. _V -> ( { 0 , n } = { 0 , 1 } <-> n = 1 ) )
69 41 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 39 70 bitri 
 |-  ( ( { 0 , n } = { 0 , 1 } \/ { 0 , n } = { 1 , 2 } \/ { 0 , n } = { 2 , 3 } ) <-> n = 1 )
72 4nn0 
 |-  4 e. NN0
73 15 72 pm3.2i 
 |-  ( 3 e. _V /\ 4 e. NN0 )
74 40 73 pm3.2i 
 |-  ( ( 0 e. _V /\ n e. _V ) /\ ( 3 e. _V /\ 4 e. NN0 ) )
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 e. _V /\ n e. _V ) /\ ( 3 e. _V /\ 4 e. NN0 ) ) -> ( ( ( 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 20 pm3.2i 
 |-  ( 4 e. NN0 /\ 5 e. NN0 )
84 40 83 pm3.2i 
 |-  ( ( 0 e. _V /\ n e. _V ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) )
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 e. _V /\ n e. _V ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 30 a1i 
 |-  ( 5 e. NN0 -> n e. _V )
96 elex 
 |-  ( 5 e. NN0 -> 5 e. _V )
97 95 96 preq2b 
 |-  ( 5 e. NN0 -> ( { 0 , n } = { 0 , 5 } <-> n = 5 ) )
98 20 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 38 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 34 101 bitri 
 |-  ( { 0 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) <-> ( n = 3 \/ ( n = 1 \/ n = 5 ) ) )
103 29 31 102 3bitr4i 
 |-  ( n e. { 1 , 3 , 5 } <-> { 0 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) )
104 103 a1i 
 |-  ( ( ( 1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 5 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) /\ n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) -> ( n e. { 1 , 3 , 5 } <-> { 0 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
105 26 104 eqrrabd 
 |-  ( ( 1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 5 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) -> { 1 , 3 , 5 } = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { 0 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )
106 14 19 25 105 mp3an 
 |-  { 1 , 3 , 5 } = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { 0 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) }
107 10 106 eqtr4i 
 |-  ( G NeighbVtx 0 ) = { 1 , 3 , 5 }