Theorem clnbupgr

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

	Ref	Expression
Hypotheses	clnbuhgr.v	|- V = ( Vtx ` G )
	clnbuhgr.e	|- E = ( Edg ` G )
Assertion	clnbupgr	|- ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | { N , n } e. E } ) )

Proof

Step	Hyp	Ref	Expression
1		clnbuhgr.v	|- V = ( Vtx ` G )
2		clnbuhgr.e	|- E = ( Edg ` G )
3	1	dfclnbgr4	|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) )
4	3	adantl	|- ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) )
5	1 2	nbupgr	|- ( ( G e. UPGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | { N , n } e. E } )
6	5	uneq2d	|- ( ( G e. UPGraph /\ N e. V ) -> ( { N } u. ( G NeighbVtx N ) ) = ( { N } u. { n e. ( V \ { N } ) | { N , n } e. E } ) )
7		rabdif	|- ( { n e. V | { N , n } e. E } \ { N } ) = { n e. ( V \ { N } ) | { N , n } e. E }
8	7	eqcomi	|- { n e. ( V \ { N } ) | { N , n } e. E } = ( { n e. V | { N , n } e. E } \ { N } )
9	8	uneq2i	|- ( { N } u. { n e. ( V \ { N } ) | { N , n } e. E } ) = ( { N } u. ( { n e. V | { N , n } e. E } \ { N } ) )
10		undif2	|- ( { N } u. ( { n e. V | { N , n } e. E } \ { N } ) ) = ( { N } u. { n e. V | { N , n } e. E } )
11	9 10	eqtri	|- ( { N } u. { n e. ( V \ { N } ) | { N , n } e. E } ) = ( { N } u. { n e. V | { N , n } e. E } )
12	11	a1i	|- ( ( G e. UPGraph /\ N e. V ) -> ( { N } u. { n e. ( V \ { N } ) | { N , n } e. E } ) = ( { N } u. { n e. V | { N , n } e. E } ) )
13	4 6 12	3eqtrd	|- ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | { N , n } e. E } ) )