Theorem dfclnbgr3

Description: Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval ). (Contributed by AV, 8-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		dfclnbgr3.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		dfclnbgr3.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		edgval	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
4	3	eqcomi	$$⊢\mathrm{ran}\mathrm{iEdg}\left(G\right)=\mathrm{Edg}\left(G\right)$$
5	1 4	clnbgrval	Could not format ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) ) : No typesetting found for |- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) ) with typecode |-
6	5	adantr	Could not format ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) ) : No typesetting found for |- ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) ) with typecode |-
7	2	eqcomi	$$⊢\mathrm{iEdg}\left(G\right)=I$$
8	7	rneqi	$$⊢\mathrm{ran}\mathrm{iEdg}\left(G\right)=\mathrm{ran}I$$
9	8	rexeqi	$$⊢\exists e\in \mathrm{ran}\mathrm{iEdg}\left(G\right)\left\{N,n\right\}\subseteq e\leftrightarrow \exists e\in \mathrm{ran}I\left\{N,n\right\}\subseteq e$$
10		funfn	$$⊢\mathrm{Fun}I\leftrightarrow IFn\mathrm{dom}I$$
11	10	biimpi	$$⊢\mathrm{Fun}I\to IFn\mathrm{dom}I$$
12	11	adantl	$$⊢\left(N\in V\wedge \mathrm{Fun}I\right)\to IFn\mathrm{dom}I$$
13		sseq2	$$⊢e=I\left(i\right)\to \left(\left\{N,n\right\}\subseteq e\leftrightarrow \left\{N,n\right\}\subseteq I\left(i\right)\right)$$
14	13	rexrn	$$⊢IFn\mathrm{dom}I\to \left(\exists e\in \mathrm{ran}I\left\{N,n\right\}\subseteq e\leftrightarrow \exists i\in \mathrm{dom}I\left\{N,n\right\}\subseteq I\left(i\right)\right)$$
15	12 14	syl	$$⊢\left(N\in V\wedge \mathrm{Fun}I\right)\to \left(\exists e\in \mathrm{ran}I\left\{N,n\right\}\subseteq e\leftrightarrow \exists i\in \mathrm{dom}I\left\{N,n\right\}\subseteq I\left(i\right)\right)$$
16	9 15	bitrid	$$⊢\left(N\in V\wedge \mathrm{Fun}I\right)\to \left(\exists e\in \mathrm{ran}\mathrm{iEdg}\left(G\right)\left\{N,n\right\}\subseteq e\leftrightarrow \exists i\in \mathrm{dom}I\left\{N,n\right\}\subseteq I\left(i\right)\right)$$
17	16	rabbidv	$$⊢\left(N\in V\wedge \mathrm{Fun}I\right)\to \left\{n\in V|\exists e\in \mathrm{ran}\mathrm{iEdg}\left(G\right)\left\{N,n\right\}\subseteq e\right\}=\left\{n\in V|\exists i\in \mathrm{dom}I\left\{N,n\right\}\subseteq I\left(i\right)\right\}$$
18	17	uneq2d	$$⊢\left(N\in V\wedge \mathrm{Fun}I\right)\to \left\{N\right\}\cup \left\{n\in V|\exists e\in \mathrm{ran}\mathrm{iEdg}\left(G\right)\left\{N,n\right\}\subseteq e\right\}=\left\{N\right\}\cup \left\{n\in V|\exists i\in \mathrm{dom}I\left\{N,n\right\}\subseteq I\left(i\right)\right\}$$
19	6 18	eqtrd	Could not format ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } ) ) : No typesetting found for |- ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } ) ) with typecode |-