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