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