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 e. ( G ClNeighbVtx K ) <-> K e. ( G ClNeighbVtx N ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( N e. ( Vtx ` G ) /\ K e. ( Vtx ` G ) ) <-> ( K e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) )
2		eqcom	|- ( N = K <-> K = N )
3		prcom	|- { K , N } = { N , K }
4	3	sseq1i	|- ( { K , N } C_ e <-> { N , K } C_ e )
5	4	rexbii	|- ( E. e e. ( Edg ` G ) { K , N } C_ e <-> E. e e. ( Edg ` G ) { N , K } C_ e )
6	2 5	orbi12i	|- ( ( N = K \/ E. e e. ( Edg ` G ) { K , N } C_ e ) <-> ( K = N \/ E. e e. ( Edg ` G ) { N , K } C_ e ) )
7	1 6	anbi12i	|- ( ( ( N e. ( Vtx ` G ) /\ K e. ( Vtx ` G ) ) /\ ( N = K \/ E. e e. ( Edg ` G ) { K , N } C_ e ) ) <-> ( ( K e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) /\ ( K = N \/ E. e e. ( Edg ` G ) { N , K } C_ e ) ) )
8		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
9		eqid	|- ( Edg ` G ) = ( Edg ` G )
10	8 9	clnbgrel	|- ( N e. ( G ClNeighbVtx K ) <-> ( ( N e. ( Vtx ` G ) /\ K e. ( Vtx ` G ) ) /\ ( N = K \/ E. e e. ( Edg ` G ) { K , N } C_ e ) ) )
11	8 9	clnbgrel	|- ( K e. ( G ClNeighbVtx N ) <-> ( ( K e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) /\ ( K = N \/ E. e e. ( Edg ` G ) { N , K } C_ e ) ) )
12	7 10 11	3bitr4i	|- ( N e. ( G ClNeighbVtx K ) <-> K e. ( G ClNeighbVtx N ) )