Metamath Proof Explorer

Theorem usgrexmpl2nb4

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