Theorem clnbupgr

Description: The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025)

	Ref	Expression
Hypotheses	clnbuhgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	clnbuhgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	clnbupgr	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )

Proof

Step	Hyp	Ref	Expression
1		clnbuhgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clnbuhgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1	dfclnbgr4	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
4	3	adantl	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) )
5	1 2	nbupgr	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
6	5	uneq2d	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( { 𝑁 } ∪ ( 𝐺 NeighbVtx 𝑁 ) ) = ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )
7		rabdif	⊢ ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ∖ { 𝑁 } ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 }
8	7	eqcomi	⊢ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } = ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ∖ { 𝑁 } )
9	8	uneq2i	⊢ ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) = ( { 𝑁 } ∪ ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ∖ { 𝑁 } ) )
10		undif2	⊢ ( { 𝑁 } ∪ ( { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ∖ { 𝑁 } ) ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
11	9 10	eqtri	⊢ ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
12	11	a1i	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( { 𝑁 } ∪ { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )
13	4 6 12	3eqtrd	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝑁 ) = ( { 𝑁 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )