Theorem clnbupgr

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

	Ref	Expression
Hypotheses	clnbuhgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	clnbuhgr.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	clnbupgr	Could not format assertion : No typesetting found for |- ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | { N , n } e. E } ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		clnbuhgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		clnbuhgr.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3	1	dfclnbgr4	Could not format ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) ) : No typesetting found for |- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) ) with typecode |-
4	3	adantl	Could not format ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) ) : No typesetting found for |- ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) ) with typecode |-
5	1 2	nbupgr	$$⊢\left(G\in \mathrm{UPGraph}\wedge N\in V\right)\to G\mathrm{NeighbVtx}N=\left\{n\in \left(V\setminus \left\{N\right\}\right)|\left\{N,n\right\}\in E\right\}$$
6	5	uneq2d	$$⊢\left(G\in \mathrm{UPGraph}\wedge N\in V\right)\to \left\{N\right\}\cup \left(G\mathrm{NeighbVtx}N\right)=\left\{N\right\}\cup \left\{n\in \left(V\setminus \left\{N\right\}\right)|\left\{N,n\right\}\in E\right\}$$
7		rabdif	$$⊢\left\{n\in V|\left\{N,n\right\}\in E\right\}\setminus \left\{N\right\}=\left\{n\in \left(V\setminus \left\{N\right\}\right)|\left\{N,n\right\}\in E\right\}$$
8	7	eqcomi	$$⊢\left\{n\in \left(V\setminus \left\{N\right\}\right)|\left\{N,n\right\}\in E\right\}=\left\{n\in V|\left\{N,n\right\}\in E\right\}\setminus \left\{N\right\}$$
9	8	uneq2i	$$⊢\left\{N\right\}\cup \left\{n\in \left(V\setminus \left\{N\right\}\right)|\left\{N,n\right\}\in E\right\}=\left\{N\right\}\cup \left(\left\{n\in V|\left\{N,n\right\}\in E\right\}\setminus \left\{N\right\}\right)$$
10		undif2	$$⊢\left\{N\right\}\cup \left(\left\{n\in V|\left\{N,n\right\}\in E\right\}\setminus \left\{N\right\}\right)=\left\{N\right\}\cup \left\{n\in V|\left\{N,n\right\}\in E\right\}$$
11	9 10	eqtri	$$⊢\left\{N\right\}\cup \left\{n\in \left(V\setminus \left\{N\right\}\right)|\left\{N,n\right\}\in E\right\}=\left\{N\right\}\cup \left\{n\in V|\left\{N,n\right\}\in E\right\}$$
12	11	a1i	$$⊢\left(G\in \mathrm{UPGraph}\wedge N\in V\right)\to \left\{N\right\}\cup \left\{n\in \left(V\setminus \left\{N\right\}\right)|\left\{N,n\right\}\in E\right\}=\left\{N\right\}\cup \left\{n\in V|\left\{N,n\right\}\in E\right\}$$
13	4 6 12	3eqtrd	Could not format ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | { N , n } e. E } ) ) : No typesetting found for |- ( ( G e. UPGraph /\ N e. V ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | { N , n } e. E } ) ) with typecode |-