Theorem dfclnbgr5

Description: Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiclosed neighborhood. (Contributed by AV, 16-May-2025)

	Ref	Expression
Hypotheses	dfsclnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	dfsclnbgr2.s	⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 }
	dfsclnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	dfclnbgr5	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfsclnbgr2.s	⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 }
3		dfsclnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4	1 3	dfclnbgr2	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) )
5	1 2 3	dfsclnbgr2	⊢ ( 𝑁 ∈ 𝑉 → 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
6	5	uneq2d	⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 } ∪ 𝑆 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) )
7	4 6	eqtr4d	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ 𝑆 ) )