Metamath Proof Explorer


Theorem clnbgrel

Description: Characterization of a member N of the closed neighborhood of a vertex X in a graph G . (Contributed by AV, 9-May-2025)

Ref Expression
Hypotheses clnbgrel.v V = Vtx G
clnbgrel.e E = Edg G
Assertion clnbgrel N G ClNeighbVtx X N V X V N = X e E X N e

Proof

Step Hyp Ref Expression
1 clnbgrel.v V = Vtx G
2 clnbgrel.e E = Edg G
3 1 clnbgrcl N G ClNeighbVtx X X V
4 3 pm4.71ri N G ClNeighbVtx X X V N G ClNeighbVtx X
5 1 2 clnbgrval X V G ClNeighbVtx X = X n V | e E X n e
6 5 eleq2d X V N G ClNeighbVtx X N X n V | e E X n e
7 elun N X n V | e E X n e N X N n V | e E X n e
8 elsn2g X V N X N = X
9 preq2 n = N X n = X N
10 9 sseq1d n = N X n e X N e
11 10 rexbidv n = N e E X n e e E X N e
12 11 elrab N n V | e E X n e N V e E X N e
13 12 a1i X V N n V | e E X n e N V e E X N e
14 8 13 orbi12d X V N X N n V | e E X n e N = X N V e E X N e
15 7 14 bitrid X V N X n V | e E X n e N = X N V e E X N e
16 eleq1 N = X N V X V
17 16 biimparc X V N = X N V
18 orc N = X N = X e E X N e
19 18 adantl X V N = X N = X e E X N e
20 17 19 jca X V N = X N V N = X e E X N e
21 20 ex X V N = X N V N = X e E X N e
22 olc e E X N e N = X e E X N e
23 22 anim2i N V e E X N e N V N = X e E X N e
24 23 a1i X V N V e E X N e N V N = X e E X N e
25 21 24 jaod X V N = X N V e E X N e N V N = X e E X N e
26 orc N = X N = X N V e E X N e
27 26 a1i X V N V N = X N = X N V e E X N e
28 olc N V e E X N e N = X N V e E X N e
29 28 ex N V e E X N e N = X N V e E X N e
30 29 adantl X V N V e E X N e N = X N V e E X N e
31 27 30 jaod X V N V N = X e E X N e N = X N V e E X N e
32 31 expimpd X V N V N = X e E X N e N = X N V e E X N e
33 25 32 impbid X V N = X N V e E X N e N V N = X e E X N e
34 6 15 33 3bitrd X V N G ClNeighbVtx X N V N = X e E X N e
35 34 pm5.32i X V N G ClNeighbVtx X X V N V N = X e E X N e
36 anass X V N V N = X e E X N e X V N V N = X e E X N e
37 36 bicomi X V N V N = X e E X N e X V N V N = X e E X N e
38 ancom X V N V N V X V
39 37 38 bianbi X V N V N = X e E X N e N V X V N = X e E X N e
40 4 35 39 3bitri N G ClNeighbVtx X N V X V N = X e E X N e