Metamath Proof Explorer


Theorem clnbgrsym

Description: In a graph, the closed neighborhood relation is symmetric: a vertex N in a graph G is a neighbor of a second vertex K iff the second vertex K is a neighbor of the first vertex N . (Contributed by AV, 10-May-2025)

Ref Expression
Assertion clnbgrsym N G ClNeighbVtx K K G ClNeighbVtx N

Proof

Step Hyp Ref Expression
1 ancom N Vtx G K Vtx G K Vtx G N Vtx G
2 eqcom N = K K = N
3 prcom K N = N K
4 3 sseq1i K N e N K e
5 4 rexbii e Edg G K N e e Edg G N K e
6 2 5 orbi12i N = K e Edg G K N e K = N e Edg G N K e
7 1 6 anbi12i N Vtx G K Vtx G N = K e Edg G K N e K Vtx G N Vtx G K = N e Edg G N K e
8 eqid Vtx G = Vtx G
9 eqid Edg G = Edg G
10 8 9 clnbgrel N G ClNeighbVtx K N Vtx G K Vtx G N = K e Edg G K N e
11 8 9 clnbgrel K G ClNeighbVtx N K Vtx G N Vtx G K = N e Edg G N K e
12 7 10 11 3bitr4i N G ClNeighbVtx K K G ClNeighbVtx N