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 e. _V
5 4 tpid1 
 |-  3 e. { 3 , 4 , 5 }
6 5 olci 
 |-  ( 3 e. { 0 , 1 , 2 } \/ 3 e. { 3 , 4 , 5 } )
7 elun 
 |-  ( 3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 3 e. { 0 , 1 , 2 } \/ 3 e. { 3 , 4 , 5 } ) )
8 6 7 mpbir 
 |-  3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
9 1 2 3 usgrexmpl2nblem 
 |-  ( 3 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) -> ( G NeighbVtx 3 ) = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { 3 , 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 3 ) = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { 3 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) }
11 c0ex 
 |-  0 e. _V
12 11 tpid1 
 |-  0 e. { 0 , 1 , 2 }
13 12 orci 
 |-  ( 0 e. { 0 , 1 , 2 } \/ 0 e. { 3 , 4 , 5 } )
14 elun 
 |-  ( 0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 0 e. { 0 , 1 , 2 } \/ 0 e. { 3 , 4 , 5 } ) )
15 13 14 mpbir 
 |-  0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
16 2ex 
 |-  2 e. _V
17 16 tpid3 
 |-  2 e. { 0 , 1 , 2 }
18 17 orci 
 |-  ( 2 e. { 0 , 1 , 2 } \/ 2 e. { 3 , 4 , 5 } )
19 elun 
 |-  ( 2 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 2 e. { 0 , 1 , 2 } \/ 2 e. { 3 , 4 , 5 } ) )
20 18 19 mpbir 
 |-  2 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
21 4nn0 
 |-  4 e. NN0
22 21 elexi 
 |-  4 e. _V
23 22 tpid2 
 |-  4 e. { 3 , 4 , 5 }
24 23 olci 
 |-  ( 4 e. { 0 , 1 , 2 } \/ 4 e. { 3 , 4 , 5 } )
25 elun 
 |-  ( 4 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 4 e. { 0 , 1 , 2 } \/ 4 e. { 3 , 4 , 5 } ) )
26 24 25 mpbir 
 |-  4 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
27 tpssi 
 |-  ( ( 0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 2 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 4 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) -> { 0 , 2 , 4 } C_ ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) )
28 3orass 
 |-  ( ( n = 0 \/ n = 2 \/ n = 4 ) <-> ( n = 0 \/ ( n = 2 \/ n = 4 ) ) )
29 vex 
 |-  n e. _V
30 29 eltp 
 |-  ( n e. { 0 , 2 , 4 } <-> ( n = 0 \/ n = 2 \/ n = 4 ) )
31 prex 
 |-  { 3 , n } e. _V
32 el7g 
 |-  ( { 3 , n } e. _V -> ( { 3 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 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 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 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 e. _V -> n e. _V )
37 elex 
 |-  ( 0 e. _V -> 0 e. _V )
38 36 37 preq2b 
 |-  ( 0 e. _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 e. _V /\ n e. _V )
43 1re 
 |-  1 e. RR
44 43 16 pm3.2i 
 |-  ( 1 e. RR /\ 2 e. _V )
45 42 44 pm3.2i 
 |-  ( ( 3 e. _V /\ n e. _V ) /\ ( 1 e. RR /\ 2 e. _V ) )
46 1lt3 
 |-  1 < 3
47 43 46 gtneii 
 |-  3 =/= 1
48 2re 
 |-  2 e. RR
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 e. _V /\ n e. _V ) /\ ( 1 e. RR /\ 2 e. _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 e. _V /\ 1 e. RR )
58 42 57 pm3.2i 
 |-  ( ( 3 e. _V /\ n e. _V ) /\ ( 0 e. _V /\ 1 e. RR ) )
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 e. _V /\ n e. _V ) /\ ( 0 e. _V /\ 1 e. RR ) ) -> ( ( ( 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 e. _V -> n e. _V )
73 elex 
 |-  ( 2 e. _V -> 2 e. _V )
74 72 73 preq2b 
 |-  ( 2 e. _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 e. NN0
80 21 79 pm3.2i 
 |-  ( 4 e. NN0 /\ 5 e. NN0 )
81 42 80 pm3.2i 
 |-  ( ( 3 e. _V /\ n e. _V ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) )
82 3re 
 |-  3 e. RR
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 e. _V /\ n e. _V ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. _V /\ 5 e. NN0 )
94 42 93 pm3.2i 
 |-  ( ( 3 e. _V /\ n e. _V ) /\ ( 0 e. _V /\ 5 e. NN0 ) )
95 59 86 pm3.2i 
 |-  ( 3 =/= 0 /\ 3 =/= 5 )
96 95 orci 
 |-  ( ( 3 =/= 0 /\ 3 =/= 5 ) \/ ( n =/= 0 /\ n =/= 5 ) )
97 prneimg 
 |-  ( ( ( 3 e. _V /\ n e. _V ) /\ ( 0 e. _V /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 -> n e. _V )
104 elex 
 |-  ( 4 e. NN0 -> 4 e. _V )
105 103 104 preq2b 
 |-  ( 4 e. NN0 -> ( { 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 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) <-> ( n = 0 \/ ( n = 2 \/ n = 4 ) ) )
111 28 30 110 3bitr4i 
 |-  ( n e. { 0 , 2 , 4 } <-> { 3 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) )
112 111 a1i 
 |-  ( ( ( 0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 2 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 4 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) /\ n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) -> ( n e. { 0 , 2 , 4 } <-> { 3 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
113 27 112 eqrrabd 
 |-  ( ( 0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 2 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 4 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) -> { 0 , 2 , 4 } = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { 3 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )
114 15 20 26 113 mp3an 
 |-  { 0 , 2 , 4 } = { n e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) | { 3 , n } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) }
115 10 114 eqtr4i 
 |-  ( G NeighbVtx 3 ) = { 0 , 2 , 4 }