This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Neighbors, complete graphs and universal vertices Neighbors nbgrsym
Description: In a graph, the 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 Alexander van der Vekens , 12-Oct-2017) (Revised by AV , 27-Oct-2020)
(Revised by AV , 12-Feb-2022)
Ref
Expression
Assertion
nbgrsym ⊢ N ∈ G NeighbVtx K ↔ K ∈ G NeighbVtx N
Proof
Step
Hyp
Ref
Expression
1
ancom ⊢ N ∈ Vtx G ∧ K ∈ Vtx G ↔ K ∈ Vtx G ∧ N ∈ Vtx G
2
necom ⊢ 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
1 2 5
3anbi123i ⊢ 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
7
eqid ⊢ Vtx G = Vtx G
8
eqid ⊢ Edg G = Edg G
9
7 8
nbgrel ⊢ N ∈ G NeighbVtx K ↔ N ∈ Vtx G ∧ K ∈ Vtx G ∧ N ≠ K ∧ ∃ e ∈ Edg G K N ⊆ e
10
7 8
nbgrel ⊢ K ∈ G NeighbVtx N ↔ K ∈ Vtx G ∧ N ∈ Vtx G ∧ K ≠ N ∧ ∃ e ∈ Edg G N K ⊆ e
11
6 9 10
3bitr4i ⊢ N ∈ G NeighbVtx K ↔ K ∈ G NeighbVtx N