This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )