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

Metamath Proof Explorer

Theorem nbusgreledg

Description: A class/vertex is a neighbor of another class/vertex in a simple graph iff the vertices are endpoints of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Hypothesis nbusgreledg.e 
|- E = ( Edg ` G )
Assertion nbusgreledg 
|- ( G e. USGraph -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. E ) )

Proof

Step Hyp Ref Expression
1 nbusgreledg.e 
 |-  E = ( Edg ` G )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 1 nbusgr 
 |-  ( G e. USGraph -> ( G NeighbVtx K ) = { n e. ( Vtx ` G ) | { K , n } e. E } )
4 3 eleq2d 
 |-  ( G e. USGraph -> ( N e. ( G NeighbVtx K ) <-> N e. { n e. ( Vtx ` G ) | { K , n } e. E } ) )
5 1 2 usgrpredgv 
 |-  ( ( G e. USGraph /\ { K , N } e. E ) -> ( K e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) )
6 5 simprd 
 |-  ( ( G e. USGraph /\ { K , N } e. E ) -> N e. ( Vtx ` G ) )
7 6 ex 
 |-  ( G e. USGraph -> ( { K , N } e. E -> N e. ( Vtx ` G ) ) )
8 7 pm4.71rd 
 |-  ( G e. USGraph -> ( { K , N } e. E <-> ( N e. ( Vtx ` G ) /\ { K , N } e. E ) ) )
9 prcom 
 |-  { N , K } = { K , N }
10 9 eleq1i 
 |-  ( { N , K } e. E <-> { K , N } e. E )
11 10 a1i 
 |-  ( G e. USGraph -> ( { N , K } e. E <-> { K , N } e. E ) )
12 preq2 
 |-  ( n = N -> { K , n } = { K , N } )
13 12 eleq1d 
 |-  ( n = N -> ( { K , n } e. E <-> { K , N } e. E ) )
14 13 elrab 
 |-  ( N e. { n e. ( Vtx ` G ) | { K , n } e. E } <-> ( N e. ( Vtx ` G ) /\ { K , N } e. E ) )
15 14 a1i 
 |-  ( G e. USGraph -> ( N e. { n e. ( Vtx ` G ) | { K , n } e. E } <-> ( N e. ( Vtx ` G ) /\ { K , N } e. E ) ) )
16 8 11 15 3bitr4rd 
 |-  ( G e. USGraph -> ( N e. { n e. ( Vtx ` G ) | { K , n } e. E } <-> { N , K } e. E ) )
17 4 16 bitrd 
 |-  ( G e. USGraph -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. E ) )