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 = ( Vtx ` G )
	dfclnbgr3.i	|- I = ( iEdg ` G )
Assertion	dfclnbgr3	|- ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } ) )

Proof

Step	Hyp	Ref	Expression
1		dfclnbgr3.v	|- V = ( Vtx ` G )
2		dfclnbgr3.i	|- I = ( iEdg ` G )
3		edgval	|- ( Edg ` G ) = ran ( iEdg ` G )
4	3	eqcomi	|- ran ( iEdg ` G ) = ( Edg ` G )
5	1 4	clnbgrval	|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) )
6	5	adantr	|- ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) )
7	2	eqcomi	|- ( iEdg ` G ) = I
8	7	rneqi	|- ran ( iEdg ` G ) = ran I
9	8	rexeqi	|- ( E. e e. ran ( iEdg ` G ) { N , n } C_ e <-> E. e e. ran I { N , n } C_ e )
10		funfn	|- ( Fun I <-> I Fn dom I )
11	10	biimpi	|- ( Fun I -> I Fn dom I )
12	11	adantl	|- ( ( N e. V /\ Fun I ) -> I Fn dom I )
13		sseq2	|- ( e = ( I ` i ) -> ( { N , n } C_ e <-> { N , n } C_ ( I ` i ) ) )
14	13	rexrn	|- ( I Fn dom I -> ( E. e e. ran I { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
15	12 14	syl	|- ( ( N e. V /\ Fun I ) -> ( E. e e. ran I { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
16	9 15	bitrid	|- ( ( N e. V /\ Fun I ) -> ( E. e e. ran ( iEdg ` G ) { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
17	16	rabbidv	|- ( ( N e. V /\ Fun I ) -> { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } = { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } )
18	17	uneq2d	|- ( ( N e. V /\ Fun I ) -> ( { N } u. { n e. V | E. e e. ran ( iEdg ` G ) { N , n } C_ e } ) = ( { N } u. { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } ) )
19	6 18	eqtrd	|- ( ( N e. V /\ Fun I ) -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. i e. dom I { N , n } C_ ( I ` i ) } ) )