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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
dfvopnbgr2.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
dfvopnbgr2.u ⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
Assertion dfclnbgr6 ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 dfvopnbgr2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 dfvopnbgr2.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 dfvopnbgr2.u ⊢ 𝑈 = { 𝑛 ∈ 𝑉 ∣ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∨ ∃ 𝑒 ∈ 𝐸 ( 𝑁 = 𝑛 ∧ 𝑒 = { 𝑁 } ) ) }
4 orc ⊢ ( 𝑣 = 𝑁 → ( 𝑣 = 𝑁 ∨ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) ) )
5 4 a1d ⊢ ( 𝑣 = 𝑁 → ( 𝑁 ∈ 𝑉 → ( 𝑣 = 𝑁 ∨ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) ) ) )
6 simpl ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) → 𝑣 ≠ 𝑁 )
7 6 anim1i ⊢ ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) → ( 𝑣 ≠ 𝑁 ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
8 3anass ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ↔ ( 𝑣 ≠ 𝑁 ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
9 7 8 sylibr ⊢ ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) → ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) )
10 9 orcd ⊢ ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) → ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) )
11 10 ex ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) → ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
12 3simpc ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) )
13 12 a1i ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
14 vsnid ⊢ 𝑣 ∈ { 𝑣 }
15 eleq2 ⊢ ( 𝑒 = { 𝑣 } → ( 𝑣 ∈ 𝑒 ↔ 𝑣 ∈ { 𝑣 } ) )
16 14 15 mpbiri ⊢ ( 𝑒 = { 𝑣 } → 𝑣 ∈ 𝑒 )
17 16 adantl ⊢ ( ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) → 𝑣 ∈ 𝑒 )
18 eleq1 ⊢ ( 𝑣 = 𝑁 → ( 𝑣 ∈ 𝑒 ↔ 𝑁 ∈ 𝑒 ) )
19 18 adantr ⊢ ( ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) → ( 𝑣 ∈ 𝑒 ↔ 𝑁 ∈ 𝑒 ) )
20 17 19 mpbid ⊢ ( ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) → 𝑁 ∈ 𝑒 )
21 20 17 jca ⊢ ( ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) )
22 21 a1i ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
23 13 22 jaod ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) → ( ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) → ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
24 11 23 impbid ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ↔ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
25 24 rexbidv ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) → ( ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
26 25 anbi2d ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) )
27 26 olcd ⊢ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑣 = 𝑁 ∨ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) ) )
28 27 ex ⊢ ( 𝑣 ≠ 𝑁 → ( 𝑁 ∈ 𝑉 → ( 𝑣 = 𝑁 ∨ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) ) ) )
29 5 28 pm2.61ine ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑣 = 𝑁 ∨ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) ) )
30 orbidi ⊢ ( ( 𝑣 = 𝑁 ∨ ( ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) ) ↔ ( ( 𝑣 = 𝑁 ∨ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ) ↔ ( 𝑣 = 𝑁 ∨ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) ) )
31 29 30 sylib ⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑣 = 𝑁 ∨ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ) ↔ ( 𝑣 = 𝑁 ∨ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) ) )
32 elun ⊢ ( 𝑣 ∈ ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) ↔ ( 𝑣 ∈ { 𝑁 } ∨ 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) )
33 velsn ⊢ ( 𝑣 ∈ { 𝑁 } ↔ 𝑣 = 𝑁 )
34 eleq1 ⊢ ( 𝑛 = 𝑣 → ( 𝑛 ∈ 𝑒 ↔ 𝑣 ∈ 𝑒 ) )
35 34 anbi2d ⊢ ( 𝑛 = 𝑣 → ( ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
36 35 rexbidv ⊢ ( 𝑛 = 𝑣 → ( ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
37 36 elrab ⊢ ( 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
38 33 37 orbi12i ⊢ ( ( 𝑣 ∈ { 𝑁 } ∨ 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) ↔ ( 𝑣 = 𝑁 ∨ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ) )
39 32 38 bitri ⊢ ( 𝑣 ∈ ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) ↔ ( 𝑣 = 𝑁 ∨ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) ) )
40 elun ⊢ ( 𝑣 ∈ ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ) ↔ ( 𝑣 ∈ { 𝑁 } ∨ 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ) )
41 neeq1 ⊢ ( 𝑛 = 𝑣 → ( 𝑛 ≠ 𝑁 ↔ 𝑣 ≠ 𝑁 ) )
42 41 34 3anbi13d ⊢ ( 𝑛 = 𝑣 → ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ↔ ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ) )
43 eqeq1 ⊢ ( 𝑛 = 𝑣 → ( 𝑛 = 𝑁 ↔ 𝑣 = 𝑁 ) )
44 sneq ⊢ ( 𝑛 = 𝑣 → { 𝑛 } = { 𝑣 } )
45 44 eqeq2d ⊢ ( 𝑛 = 𝑣 → ( 𝑒 = { 𝑛 } ↔ 𝑒 = { 𝑣 } ) )
46 43 45 anbi12d ⊢ ( 𝑛 = 𝑣 → ( ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ↔ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) )
47 42 46 orbi12d ⊢ ( 𝑛 = 𝑣 → ( ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) ↔ ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
48 47 rexbidv ⊢ ( 𝑛 = 𝑣 → ( ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) ↔ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
49 48 elrab ⊢ ( 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ↔ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) )
50 33 49 orbi12i ⊢ ( ( 𝑣 ∈ { 𝑁 } ∨ 𝑣 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ) ↔ ( 𝑣 = 𝑁 ∨ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) )
51 40 50 bitri ⊢ ( 𝑣 ∈ ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ) ↔ ( 𝑣 = 𝑁 ∨ ( 𝑣 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑣 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑣 ∈ 𝑒 ) ∨ ( 𝑣 = 𝑁 ∧ 𝑒 = { 𝑣 } ) ) ) ) )
52 31 39 51 3bitr4g ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑣 ∈ ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) ↔ 𝑣 ∈ ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ) ) )
53 52 eqrdv ⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ) )
54 1 2 dfclnbgr2 ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) )
55 1 2 3 dfvopnbgr2 ⊢ ( 𝑁 ∈ 𝑉 → 𝑈 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } )
56 55 uneq2d ⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 } ∪ 𝑈 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( ( 𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) ∨ ( 𝑛 = 𝑁 ∧ 𝑒 = { 𝑛 } ) ) } ) )
57 53 54 56 3eqtr4d ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ 𝑈 ) )