Metamath Proof Explorer

Theorem nbupgrel

Description: A neighbor of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v 
|- V = ( Vtx ` G )
nbuhgr.e 
|- E = ( Edg ` G )
Assertion nbupgrel 
|- ( ( ( G e. UPGraph /\ K e. V ) /\ ( N e. V /\ N =/= K ) ) -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. E ) )

Proof

Step Hyp Ref Expression
1 nbuhgr.v 
 |-  V = ( Vtx ` G )
2 nbuhgr.e 
 |-  E = ( Edg ` G )
3 1 2 nbupgr 
 |-  ( ( G e. UPGraph /\ K e. V ) -> ( G NeighbVtx K ) = { n e. ( V \ { K } ) | { K , n } e. E } )
4 3 eleq2d 
 |-  ( ( G e. UPGraph /\ K e. V ) -> ( N e. ( G NeighbVtx K ) <-> N e. { n e. ( V \ { K } ) | { K , n } e. E } ) )
5 preq2 
 |-  ( n = N -> { K , n } = { K , N } )
6 5 eleq1d 
 |-  ( n = N -> ( { K , n } e. E <-> { K , N } e. E ) )
7 6 elrab 
 |-  ( N e. { n e. ( V \ { K } ) | { K , n } e. E } <-> ( N e. ( V \ { K } ) /\ { K , N } e. E ) )
8 4 7 bitrdi 
 |-  ( ( G e. UPGraph /\ K e. V ) -> ( N e. ( G NeighbVtx K ) <-> ( N e. ( V \ { K } ) /\ { K , N } e. E ) ) )
9 8 adantr 
 |-  ( ( ( G e. UPGraph /\ K e. V ) /\ ( N e. V /\ N =/= K ) ) -> ( N e. ( G NeighbVtx K ) <-> ( N e. ( V \ { K } ) /\ { K , N } e. E ) ) )
10 eldifsn 
 |-  ( N e. ( V \ { K } ) <-> ( N e. V /\ N =/= K ) )
11 10 biimpri 
 |-  ( ( N e. V /\ N =/= K ) -> N e. ( V \ { K } ) )
12 11 adantl 
 |-  ( ( ( G e. UPGraph /\ K e. V ) /\ ( N e. V /\ N =/= K ) ) -> N e. ( V \ { K } ) )
13 12 biantrurd 
 |-  ( ( ( G e. UPGraph /\ K e. V ) /\ ( N e. V /\ N =/= K ) ) -> ( { K , N } e. E <-> ( N e. ( V \ { K } ) /\ { K , N } e. E ) ) )
14 prcom 
 |-  { K , N } = { N , K }
15 14 eleq1i 
 |-  ( { K , N } e. E <-> { N , K } e. E )
16 15 a1i 
 |-  ( ( ( G e. UPGraph /\ K e. V ) /\ ( N e. V /\ N =/= K ) ) -> ( { K , N } e. E <-> { N , K } e. E ) )
17 9 13 16 3bitr2d 
 |-  ( ( ( G e. UPGraph /\ K e. V ) /\ ( N e. V /\ N =/= K ) ) -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. E ) )