Metamath Proof Explorer

Theorem usgrexmpl2nb2

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

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