Theorem clnbgrval

Description: The closed neighborhood of a vertex V in a graph G . (Contributed by AV, 7-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		clnbgrval.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		clnbgrval.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		df-clnbgr	Could not format ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) : No typesetting found for |- ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) with typecode |-
4	1	1vgrex	$$⊢N\in V\to G\in \mathrm{V}$$
5		fveq2	$$⊢G=g\to \mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(g\right)$$
6	5	eqcoms	$$⊢g=G\to \mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(g\right)$$
7	1 6	eqtrid	$$⊢g=G\to V=\mathrm{Vtx}\left(g\right)$$
8	7	eleq2d	$$⊢g=G\to \left(N\in V\leftrightarrow N\in \mathrm{Vtx}\left(g\right)\right)$$
9	8	biimpac	$$⊢\left(N\in V\wedge g=G\right)\to N\in \mathrm{Vtx}\left(g\right)$$
10		vsnex	$$⊢\left\{v\right\}\in \mathrm{V}$$
11	10	a1i	$$⊢\left(N\in V\wedge \left(g=G\wedge v=N\right)\right)\to \left\{v\right\}\in \mathrm{V}$$
12		fvex	$$⊢\mathrm{Vtx}\left(g\right)\in \mathrm{V}$$
13		rabexg	$$⊢\mathrm{Vtx}\left(g\right)\in \mathrm{V}\to \left\{n\in \mathrm{Vtx}\left(g\right)|\exists e\in \mathrm{Edg}\left(g\right)\left\{v,n\right\}\subseteq e\right\}\in \mathrm{V}$$
14	12 13	mp1i	$$⊢\left(N\in V\wedge \left(g=G\wedge v=N\right)\right)\to \left\{n\in \mathrm{Vtx}\left(g\right)|\exists e\in \mathrm{Edg}\left(g\right)\left\{v,n\right\}\subseteq e\right\}\in \mathrm{V}$$
15	11 14	unexd	$$⊢\left(N\in V\wedge \left(g=G\wedge v=N\right)\right)\to \left\{v\right\}\cup \left\{n\in \mathrm{Vtx}\left(g\right)|\exists e\in \mathrm{Edg}\left(g\right)\left\{v,n\right\}\subseteq e\right\}\in \mathrm{V}$$
16		sneq	$$⊢v=N\to \left\{v\right\}=\left\{N\right\}$$
17	16	adantl	$$⊢\left(g=G\wedge v=N\right)\to \left\{v\right\}=\left\{N\right\}$$
18		fveq2	$$⊢g=G\to \mathrm{Vtx}\left(g\right)=\mathrm{Vtx}\left(G\right)$$
19	18 1	eqtr4di	$$⊢g=G\to \mathrm{Vtx}\left(g\right)=V$$
20	19	adantr	$$⊢\left(g=G\wedge v=N\right)\to \mathrm{Vtx}\left(g\right)=V$$
21		fveq2	$$⊢g=G\to \mathrm{Edg}\left(g\right)=\mathrm{Edg}\left(G\right)$$
22	21 2	eqtr4di	$$⊢g=G\to \mathrm{Edg}\left(g\right)=E$$
23	22	adantr	$$⊢\left(g=G\wedge v=N\right)\to \mathrm{Edg}\left(g\right)=E$$
24		preq1	$$⊢v=N\to \left\{v,n\right\}=\left\{N,n\right\}$$
25	24	sseq1d	$$⊢v=N\to \left(\left\{v,n\right\}\subseteq e\leftrightarrow \left\{N,n\right\}\subseteq e\right)$$
26	25	adantl	$$⊢\left(g=G\wedge v=N\right)\to \left(\left\{v,n\right\}\subseteq e\leftrightarrow \left\{N,n\right\}\subseteq e\right)$$
27	23 26	rexeqbidv	$$⊢\left(g=G\wedge v=N\right)\to \left(\exists e\in \mathrm{Edg}\left(g\right)\left\{v,n\right\}\subseteq e\leftrightarrow \exists e\in E\left\{N,n\right\}\subseteq e\right)$$
28	20 27	rabeqbidv	$$⊢\left(g=G\wedge v=N\right)\to \left\{n\in \mathrm{Vtx}\left(g\right)|\exists e\in \mathrm{Edg}\left(g\right)\left\{v,n\right\}\subseteq e\right\}=\left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
29	17 28	uneq12d	$$⊢\left(g=G\wedge v=N\right)\to \left\{v\right\}\cup \left\{n\in \mathrm{Vtx}\left(g\right)|\exists e\in \mathrm{Edg}\left(g\right)\left\{v,n\right\}\subseteq e\right\}=\left\{N\right\}\cup \left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
30	29	adantl	$$⊢\left(N\in V\wedge \left(g=G\wedge v=N\right)\right)\to \left\{v\right\}\cup \left\{n\in \mathrm{Vtx}\left(g\right)|\exists e\in \mathrm{Edg}\left(g\right)\left\{v,n\right\}\subseteq e\right\}=\left\{N\right\}\cup \left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
31	4 9 15 30	ovmpodv2	Could not format ( N e. V -> ( ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E { N , n } C_ e } ) ) ) : No typesetting found for |- ( N e. V -> ( ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E { N , n } C_ e } ) ) ) with typecode |-
32	3 31	mpi	Could not format ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E { N , n } C_ e } ) ) : No typesetting found for |- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E { N , n } C_ e } ) ) with typecode |-