Metamath Proof Explorer

Theorem 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