Metamath Proof Explorer


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 V Fun I G ClNeighbVtx N = N n V | i dom I N n 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 V G ClNeighbVtx N = N n V | e ran iEdg G N n e
6 5 adantr N V Fun I G ClNeighbVtx N = N n V | e ran iEdg G N n e
7 2 eqcomi iEdg G = I
8 7 rneqi ran iEdg G = ran I
9 8 rexeqi e ran iEdg G N n e e ran I N n e
10 funfn Fun I I Fn dom I
11 10 biimpi Fun I I Fn dom I
12 11 adantl N V Fun I I Fn dom I
13 sseq2 e = I i N n e N n I i
14 13 rexrn I Fn dom I e ran I N n e i dom I N n I i
15 12 14 syl N V Fun I e ran I N n e i dom I N n I i
16 9 15 bitrid N V Fun I e ran iEdg G N n e i dom I N n I i
17 16 rabbidv N V Fun I n V | e ran iEdg G N n e = n V | i dom I N n I i
18 17 uneq2d N V Fun I N n V | e ran iEdg G N n e = N n V | i dom I N n I i
19 6 18 eqtrd N V Fun I G ClNeighbVtx N = N n V | i dom I N n I i