Metamath Proof Explorer

Theorem dfnbgr6

Description: Alternate definition of the (open) neighborhood of a vertex as a difference of its semiopen neighborhood and the singleton of itself. (Contributed by AV, 17-May-2025)

Ref Expression
Hypotheses dfvopnbgr2.v 
|- V = ( Vtx ` G )
dfvopnbgr2.e 
|- E = ( Edg ` G )
dfvopnbgr2.u 
|- U = { n e. V | ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) }
Assertion dfnbgr6 
|- ( N e. V -> ( G NeighbVtx N ) = ( U \ { N } ) )

Proof

Step Hyp Ref Expression
1 dfvopnbgr2.v 
 |-  V = ( Vtx ` G )
2 dfvopnbgr2.e 
 |-  E = ( Edg ` G )
3 dfvopnbgr2.u 
 |-  U = { n e. V | ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) }
4 rabdif 
 |-  ( { n e. V | E. e e. E ( N e. e /\ n e. e ) } \ { N } ) = { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) }
5 3anass 
 |-  ( ( v =/= N /\ N e. e /\ v e. e ) <-> ( v =/= N /\ ( N e. e /\ v e. e ) ) )
6 5 biimpri 
 |-  ( ( v =/= N /\ ( N e. e /\ v e. e ) ) -> ( v =/= N /\ N e. e /\ v e. e ) )
7 6 orcd 
 |-  ( ( v =/= N /\ ( N e. e /\ v e. e ) ) -> ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) )
8 7 ex 
 |-  ( v =/= N -> ( ( N e. e /\ v e. e ) -> ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
9 3simpc 
 |-  ( ( v =/= N /\ N e. e /\ v e. e ) -> ( N e. e /\ v e. e ) )
10 9 a1i 
 |-  ( v =/= N -> ( ( v =/= N /\ N e. e /\ v e. e ) -> ( N e. e /\ v e. e ) ) )
11 eqneqall 
 |-  ( v = N -> ( v =/= N -> ( e = { v } -> ( N e. e /\ v e. e ) ) ) )
12 11 com12 
 |-  ( v =/= N -> ( v = N -> ( e = { v } -> ( N e. e /\ v e. e ) ) ) )
13 12 impd 
 |-  ( v =/= N -> ( ( v = N /\ e = { v } ) -> ( N e. e /\ v e. e ) ) )
14 10 13 jaod 
 |-  ( v =/= N -> ( ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) -> ( N e. e /\ v e. e ) ) )
15 8 14 impbid 
 |-  ( v =/= N -> ( ( N e. e /\ v e. e ) <-> ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
16 15 rexbidv 
 |-  ( v =/= N -> ( E. e e. E ( N e. e /\ v e. e ) <-> E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
17 16 anbi2d 
 |-  ( v =/= N -> ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) )
18 17 pm5.32ri 
 |-  ( ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) /\ v =/= N ) <-> ( ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) /\ v =/= N ) )
19 18 a1i 
 |-  ( N e. V -> ( ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) /\ v =/= N ) <-> ( ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) /\ v =/= N ) ) )
20 eldif 
 |-  ( v e. ( { n e. V | E. e e. E ( N e. e /\ n e. e ) } \ { N } ) <-> ( v e. { n e. V | E. e e. E ( N e. e /\ n e. e ) } /\ -. v e. { N } ) )
21 elequ1 
 |-  ( n = v -> ( n e. e <-> v e. e ) )
22 21 anbi2d 
 |-  ( n = v -> ( ( N e. e /\ n e. e ) <-> ( N e. e /\ v e. e ) ) )
23 22 rexbidv 
 |-  ( n = v -> ( E. e e. E ( N e. e /\ n e. e ) <-> E. e e. E ( N e. e /\ v e. e ) ) )
24 23 elrab 
 |-  ( v e. { n e. V | E. e e. E ( N e. e /\ n e. e ) } <-> ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) )
25 velsn 
 |-  ( v e. { N } <-> v = N )
26 25 necon3bbii 
 |-  ( -. v e. { N } <-> v =/= N )
27 24 26 anbi12i 
 |-  ( ( v e. { n e. V | E. e e. E ( N e. e /\ n e. e ) } /\ -. v e. { N } ) <-> ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) /\ v =/= N ) )
28 20 27 bitri 
 |-  ( v e. ( { n e. V | E. e e. E ( N e. e /\ n e. e ) } \ { N } ) <-> ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) /\ v =/= N ) )
29 eldif 
 |-  ( v e. ( { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } \ { N } ) <-> ( v e. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } /\ -. v e. { N } ) )
30 neeq1 
 |-  ( n = v -> ( n =/= N <-> v =/= N ) )
31 30 21 3anbi13d 
 |-  ( n = v -> ( ( n =/= N /\ N e. e /\ n e. e ) <-> ( v =/= N /\ N e. e /\ v e. e ) ) )
32 eqeq1 
 |-  ( n = v -> ( n = N <-> v = N ) )
33 sneq 
 |-  ( n = v -> { n } = { v } )
34 33 eqeq2d 
 |-  ( n = v -> ( e = { n } <-> e = { v } ) )
35 32 34 anbi12d 
 |-  ( n = v -> ( ( n = N /\ e = { n } ) <-> ( v = N /\ e = { v } ) ) )
36 31 35 orbi12d 
 |-  ( n = v -> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) <-> ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
37 36 rexbidv 
 |-  ( n = v -> ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) <-> E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
38 37 elrab 
 |-  ( v e. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
39 38 26 anbi12i 
 |-  ( ( v e. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } /\ -. v e. { N } ) <-> ( ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) /\ v =/= N ) )
40 29 39 bitri 
 |-  ( v e. ( { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } \ { N } ) <-> ( ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) /\ v =/= N ) )
41 19 28 40 3bitr4g 
 |-  ( N e. V -> ( v e. ( { n e. V | E. e e. E ( N e. e /\ n e. e ) } \ { N } ) <-> v e. ( { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } \ { N } ) ) )
42 41 eqrdv 
 |-  ( N e. V -> ( { n e. V | E. e e. E ( N e. e /\ n e. e ) } \ { N } ) = ( { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } \ { N } ) )
43 4 42 eqtr3id 
 |-  ( N e. V -> { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) } = ( { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } \ { N } ) )
44 1 2 dfnbgr2 
 |-  ( N e. V -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) } )
45 1 2 3 dfvopnbgr2 
 |-  ( N e. V -> U = { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } )
46 45 difeq1d 
 |-  ( N e. V -> ( U \ { N } ) = ( { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } \ { N } ) )
47 43 44 46 3eqtr4d 
 |-  ( N e. V -> ( G NeighbVtx N ) = ( U \ { N } ) )