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 e. ( G NeighbVtx K ) <-> K e. ( G NeighbVtx 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 necom 
 |-  ( 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 1 2 5 3anbi123i 
 |-  ( ( ( 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 ) )
7 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
9 7 8 nbgrel 
 |-  ( N e. ( G NeighbVtx K ) <-> ( ( N e. ( Vtx ` G ) /\ K e. ( Vtx ` G ) ) /\ N =/= K /\ E. e e. ( Edg ` G ) { K , N } C_ e ) )
10 7 8 nbgrel 
 |-  ( K e. ( G NeighbVtx N ) <-> ( ( K e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) /\ K =/= N /\ E. e e. ( Edg ` G ) { N , K } C_ e ) )
11 6 9 10 3bitr4i 
 |-  ( N e. ( G NeighbVtx K ) <-> K e. ( G NeighbVtx N ) )