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