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