Theorem dfclnbgr4

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

	Ref	Expression
Hypothesis	dfclnbgr4.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	dfclnbgr4	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfclnbgr4.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3	1 2	dfclnbgr2	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) )
4		undif2	⊢ ( { 𝑁 } ∪ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
5		rabdif	⊢ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) }
6	5	uneq2i	⊢ ( { 𝑁 } ∪ ( { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ∖ { 𝑁 } ) ) = ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
7	4 6	eqtr3i	⊢ ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) = ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
8	1 2	dfnbgr2	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } )
9	8	eqcomd	⊢ ( 𝑁 ∈ 𝑉 → { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } = ( 𝐺 NeighbVtx 𝑁 ) )
10	9	uneq2d	⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
11	7 10	eqtrid	⊢ ( 𝑁 ∈ 𝑉 → ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) ( 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒 ) } ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
12	3 11	eqtrd	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )