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 1ex 
 |-  1 e. _V
12 11 tpid2 
 |-  1 e. { 0 , 1 , 2 }
13 12 orci 
 |-  ( 1 e. { 0 , 1 , 2 } \/ 1 e. { 3 , 4 , 5 } )
14 elun 
 |-  ( 1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 1 e. { 0 , 1 , 2 } \/ 1 e. { 3 , 4 , 5 } ) )
15 13 14 mpbir 
 |-  1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
16 3ex 
 |-  3 e. _V
17 16 tpid1 
 |-  3 e. { 3 , 4 , 5 }
18 17 olci 
 |-  ( 3 e. { 0 , 1 , 2 } \/ 3 e. { 3 , 4 , 5 } )
19 elun 
 |-  ( 3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 3 e. { 0 , 1 , 2 } \/ 3 e. { 3 , 4 , 5 } ) )
20 18 19 mpbir 
 |-  3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
21 5nn0 
 |-  5 e. NN0
22 21 elexi 
 |-  5 e. _V
23 22 tpid3 
 |-  5 e. { 3 , 4 , 5 }
24 23 olci 
 |-  ( 5 e. { 0 , 1 , 2 } \/ 5 e. { 3 , 4 , 5 } )
25 elun 
 |-  ( 5 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 5 e. { 0 , 1 , 2 } \/ 5 e. { 3 , 4 , 5 } ) )
26 24 25 mpbir 
 |-  5 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
27 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 } ) )
28 3orcoma 
 |-  ( ( n = 3 \/ n = 1 \/ n = 5 ) <-> ( n = 1 \/ n = 3 \/ n = 5 ) )
29 3orass 
 |-  ( ( n = 3 \/ n = 1 \/ n = 5 ) <-> ( n = 3 \/ ( n = 1 \/ n = 5 ) ) )
30 28 29 bitr3i 
 |-  ( ( n = 1 \/ n = 3 \/ n = 5 ) <-> ( n = 3 \/ ( n = 1 \/ n = 5 ) ) )
31 vex 
 |-  n e. _V
32 31 eltp 
 |-  ( n e. { 1 , 3 , 5 } <-> ( n = 1 \/ n = 3 \/ n = 5 ) )
33 prex 
 |-  { 0 , n } e. _V
34 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 } ) ) ) ) )
35 33 34 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 } ) ) ) )
36 31 a1i 
 |-  ( 3 e. _V -> n e. _V )
37 elex 
 |-  ( 3 e. _V -> 3 e. _V )
38 36 37 preq2b 
 |-  ( 3 e. _V -> ( { 0 , n } = { 0 , 3 } <-> n = 3 ) )
39 16 38 ax-mp 
 |-  ( { 0 , n } = { 0 , 3 } <-> n = 3 )
40 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 } ) )
41 4 31 pm3.2i 
 |-  ( 0 e. _V /\ n e. _V )
42 2ex 
 |-  2 e. _V
43 11 42 pm3.2i 
 |-  ( 1 e. _V /\ 2 e. _V )
44 41 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 16 pm3.2i 
 |-  ( 2 e. _V /\ 3 e. _V )
54 41 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 31 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 11 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 40 70 bitri 
 |-  ( ( { 0 , n } = { 0 , 1 } \/ { 0 , n } = { 1 , 2 } \/ { 0 , n } = { 2 , 3 } ) <-> n = 1 )
72 4nn0 
 |-  4 e. NN0
73 16 72 pm3.2i 
 |-  ( 3 e. _V /\ 4 e. NN0 )
74 41 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 21 pm3.2i 
 |-  ( 4 e. NN0 /\ 5 e. NN0 )
84 41 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 31 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 21 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 39 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 35 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 30 32 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 27 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 15 20 26 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 }