Metamath Proof Explorer

Theorem usgrexmpl2nb5

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