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	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ 𝐾 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	⊢ ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) ↔ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
2		eqcom	⊢ ( 𝑁 = 𝐾 ↔ 𝐾 = 𝑁 )
3		prcom	⊢ { 𝐾 , 𝑁 } = { 𝑁 , 𝐾 }
4	3	sseq1i	⊢ ( { 𝐾 , 𝑁 } ⊆ 𝑒 ↔ { 𝑁 , 𝐾 } ⊆ 𝑒 )
5	4	rexbii	⊢ ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 )
6	2 5	orbi12i	⊢ ( ( 𝑁 = 𝐾 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) ↔ ( 𝐾 = 𝑁 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 ) )
7	1 6	anbi12i	⊢ ( ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑁 = 𝐾 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) ) ↔ ( ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐾 = 𝑁 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 ) ) )
8		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
9		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
10	8 9	clnbgrel	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ ( ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑁 = 𝐾 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑁 } ⊆ 𝑒 ) ) )
11	8 9	clnbgrel	⊢ ( 𝐾 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) ↔ ( ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐾 = 𝑁 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑁 , 𝐾 } ⊆ 𝑒 ) ) )
12	7 10 11	3bitr4i	⊢ ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ 𝐾 ∈ ( 𝐺 ClNeighbVtx 𝑁 ) )