Metamath Proof Explorer

Theorem dfclnbgr6

Description: Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiopen neighborhood. (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 dfclnbgr6 ⊢ N ∈ V → G ClNeighbVtx N = N ∪ U

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 orc ⊢ v = N → v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
5 4 a1d ⊢ v = N → N ∈ V → v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
6 simpl ⊢ v ≠ N ∧ N ∈ V → v ≠ N
7 6 anim1i ⊢ v ≠ N ∧ N ∈ V ∧ N ∈ e ∧ v ∈ e → v ≠ N ∧ N ∈ e ∧ v ∈ e
8 3anass ⊢ v ≠ N ∧ N ∈ e ∧ v ∈ e ↔ v ≠ N ∧ N ∈ e ∧ v ∈ e
9 7 8 sylibr ⊢ v ≠ N ∧ N ∈ V ∧ N ∈ e ∧ v ∈ e → v ≠ N ∧ N ∈ e ∧ v ∈ e
10 9 orcd ⊢ v ≠ N ∧ N ∈ V ∧ N ∈ e ∧ v ∈ e → v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
11 10 ex ⊢ v ≠ N ∧ N ∈ V → N ∈ e ∧ v ∈ e → v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
12 3simpc ⊢ v ≠ N ∧ N ∈ e ∧ v ∈ e → N ∈ e ∧ v ∈ e
13 12 a1i ⊢ v ≠ N ∧ N ∈ V → v ≠ N ∧ N ∈ e ∧ v ∈ e → N ∈ e ∧ v ∈ e
14 vsnid ⊢ v ∈ v
15 eleq2 ⊢ e = v → v ∈ e ↔ v ∈ v
16 14 15 mpbiri ⊢ e = v → v ∈ e
17 16 adantl ⊢ v = N ∧ e = v → v ∈ e
18 eleq1 ⊢ v = N → v ∈ e ↔ N ∈ e
19 18 adantr ⊢ v = N ∧ e = v → v ∈ e ↔ N ∈ e
20 17 19 mpbid ⊢ v = N ∧ e = v → N ∈ e
21 20 17 jca ⊢ v = N ∧ e = v → N ∈ e ∧ v ∈ e
22 21 a1i ⊢ v ≠ N ∧ N ∈ V → v = N ∧ e = v → N ∈ e ∧ v ∈ e
23 13 22 jaod ⊢ v ≠ N ∧ N ∈ V → v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v → N ∈ e ∧ v ∈ e
24 11 23 impbid ⊢ v ≠ N ∧ N ∈ V → N ∈ e ∧ v ∈ e ↔ v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
25 24 rexbidv ⊢ v ≠ N ∧ N ∈ V → ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
26 25 anbi2d ⊢ v ≠ N ∧ N ∈ V → v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
27 26 olcd ⊢ v ≠ N ∧ N ∈ V → v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
28 27 ex ⊢ v ≠ N → N ∈ V → v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
29 5 28 pm2.61ine ⊢ N ∈ V → v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
30 orbidi ⊢ v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v ↔ v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v = N ∨ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
31 29 30 sylib ⊢ N ∈ V → v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e ↔ v = N ∨ v ∈ V ∧ ∃ e ∈ E v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
32 elun ⊢ v ∈ N ∪ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ v ∈ N ∨ v ∈ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e
33 velsn ⊢ v ∈ N ↔ v = N
34 eleq1 ⊢ n = v → n ∈ e ↔ v ∈ e
35 34 anbi2d ⊢ n = v → N ∈ e ∧ n ∈ e ↔ N ∈ e ∧ v ∈ e
36 35 rexbidv ⊢ n = v → ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ ∃ e ∈ E N ∈ e ∧ v ∈ e
37 36 elrab ⊢ v ∈ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e
38 33 37 orbi12i ⊢ v ∈ N ∨ v ∈ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e
39 32 38 bitri ⊢ v ∈ N ∪ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ v = N ∨ v ∈ V ∧ ∃ e ∈ E N ∈ e ∧ v ∈ e
40 elun ⊢ v ∈ N ∪ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ↔ v ∈ N ∨ v ∈ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
41 neeq1 ⊢ n = v → n ≠ N ↔ v ≠ N
42 41 34 3anbi13d ⊢ n = v → n ≠ N ∧ N ∈ e ∧ n ∈ e ↔ v ≠ N ∧ N ∈ e ∧ v ∈ e
43 eqeq1 ⊢ n = v → n = N ↔ v = N
44 sneq ⊢ n = v → n = v
45 44 eqeq2d ⊢ n = v → e = n ↔ e = v
46 43 45 anbi12d ⊢ n = v → n = N ∧ e = n ↔ v = N ∧ e = v
47 42 46 orbi12d ⊢ n = v → n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n ↔ v ≠ N ∧ N ∈ e ∧ v ∈ e ∨ v = N ∧ e = v
48 47 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
49 48 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
50 33 49 orbi12i ⊢ v ∈ N ∨ 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
51 40 50 bitri ⊢ v ∈ N ∪ 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
52 31 39 51 3bitr4g ⊢ N ∈ V → v ∈ N ∪ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e ↔ v ∈ N ∪ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
53 52 eqrdv ⊢ N ∈ V → N ∪ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e = N ∪ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
54 1 2 dfclnbgr2 ⊢ N ∈ V → G ClNeighbVtx N = N ∪ n ∈ V | ∃ e ∈ E N ∈ e ∧ n ∈ e
55 1 2 3 dfvopnbgr2 ⊢ N ∈ V → U = n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
56 55 uneq2d ⊢ N ∈ V → N ∪ U = N ∪ n ∈ V | ∃ e ∈ E n ≠ N ∧ N ∈ e ∧ n ∈ e ∨ n = N ∧ e = n
57 53 54 56 3eqtr4d ⊢ N ∈ V → G ClNeighbVtx N = N ∪ U