Metamath Proof Explorer

Theorem usgrexmpl2nb1

Description: The neighborhood of the second 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 usgrexmpl2nb1 
|- ( G NeighbVtx 1 ) = { 0 , 2 }

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