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 ∈ V | n ∈ G NeighbVtx N ∨ ∃ e ∈ E N = n ∧ e = N
Assertion dfnbgr6 ⊢ N ∈ 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 ∈ V | n ∈ G NeighbVtx N ∨ ∃ e ∈ E N = n ∧ e = N
4 rabdif ⊢ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∖ N = n ∈ V ∖ N | ∃ e ∈ E N ∈ e ∧ n ∈ e
5 3anass ⊢ v ≠ N ∧ N ∈ e ∧ v ∈ e ↔ v ≠ N ∧ N ∈ e ∧ v ∈ e
6 5 biimpri ⊢ v ≠ N ∧ N ∈ e ∧ v ∈ e → v ≠ N ∧ N ∈ e ∧ v ∈ e
7 6 orcd ⊢ v ≠ N ∧ N ∈ e ∧ v ∈ e → v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
8 7 ex ⊢ v ≠ N → N ∈ e ∧ v ∈ e → v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
9 3simpc ⊢ v ≠ N ∧ N ∈ e ∧ v ∈ e → N ∈ e ∧ v ∈ e
10 9 a1i ⊢ v ≠ N → v ≠ N ∧ N ∈ e ∧ v ∈ e → N ∈ e ∧ v ∈ e
11 eqneqall ⊢ v = N → v ≠ N → e = v → N ∈ e ∧ v ∈ e
12 11 com12 ⊢ v ≠ N → v = N → e = v → N ∈ e ∧ v ∈ e
13 12 impd ⊢ v ≠ N → v = N ∧ e = v → N ∈ e ∧ v ∈ e
14 10 13 jaod ⊢ v ≠ N → v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v → N ∈ e ∧ v ∈ e
15 8 14 impbid ⊢ v ≠ N → N ∈ e ∧ v ∈ e ↔ v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
16 15 rexbidv ⊢ v ≠ N → ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
17 16 anbi2d ⊢ v ≠ N → v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
18 17 pm5.32ri ⊢ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ∧ v ≠ N ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v ∧ v ≠ N
19 18 a1i ⊢ N ∈ V → v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ∧ v ≠ N ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v ∧ v ≠ N
20 eldif ⊢ v ∈ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∖ N ↔ v ∈ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∧ ¬ v ∈ N
21 elequ1 ⊢ n = v → n ∈ e ↔ v ∈ e
22 21 anbi2d ⊢ n = v → N ∈ e ∧ n ∈ e ↔ N ∈ e ∧ v ∈ e
23 22 rexbidv ⊢ n = v → ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ ∃ e ∈ E N ∈ e ∧ v ∈ e
24 23 elrab ⊢ v ∈ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e
25 velsn ⊢ v ∈ N ↔ v = N
26 25 necon3bbii ⊢ ¬ v ∈ N ↔ v ≠ N
27 24 26 anbi12i ⊢ v ∈ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∧ ¬ v ∈ N ↔ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ∧ v ≠ N
28 20 27 bitri ⊢ v ∈ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∖ N ↔ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ∧ v ≠ N
29 eldif ⊢ v ∈ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∖ N ↔ v ∈ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∧ ¬ v ∈ N
30 neeq1 ⊢ n = v → n ≠ N ↔ v ≠ N
31 30 21 3anbi13d ⊢ n = v → n ≠ N ∧ N ∈ e ∧ n ∈ e ↔ v ≠ N ∧ N ∈ e ∧ v ∈ 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 ∧ n ∈ e ∨ n = N ∧ e = n ↔ v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
37 36 rexbidv ⊢ n = v → ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ↔ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
38 37 elrab ⊢ v ∈ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
39 38 26 anbi12i ⊢ v ∈ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∧ ¬ v ∈ N ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v ∧ v ≠ N
40 29 39 bitri ⊢ v ∈ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∖ N ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v ∧ v ≠ N
41 19 28 40 3bitr4g ⊢ N ∈ V → v ∈ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∖ N ↔ v ∈ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∖ N
42 41 eqrdv ⊢ N ∈ V → n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ∖ N = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∖ N
43 4 42 eqtr3id ⊢ N ∈ V → n ∈ V ∖ N | ∃ e ∈ E N ∈ e ∧ n ∈ e = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∖ N
44 1 2 dfnbgr2 ⊢ N ∈ V → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ E N ∈ e ∧ n ∈ e
45 1 2 3 dfvopnbgr2 ⊢ N ∈ V → U = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
46 45 difeq1d ⊢ N ∈ V → U ∖ N = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ∖ N
47 43 44 46 3eqtr4d ⊢ N ∈ V → G NeighbVtx N = U ∖ N