Step |
Hyp |
Ref |
Expression |
1 |
|
uvtxel.v |
|- V = ( Vtx ` G ) |
2 |
|
isuvtx.e |
|- E = ( Edg ` G ) |
3 |
1
|
uvtxval |
|- ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) k e. ( G NeighbVtx v ) } |
4 |
1 2
|
nbgrel |
|- ( k e. ( G NeighbVtx v ) <-> ( ( k e. V /\ v e. V ) /\ k =/= v /\ E. e e. E { v , k } C_ e ) ) |
5 |
|
df-3an |
|- ( ( ( k e. V /\ v e. V ) /\ k =/= v /\ E. e e. E { v , k } C_ e ) <-> ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) ) |
6 |
4 5
|
bitri |
|- ( k e. ( G NeighbVtx v ) <-> ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) ) |
7 |
|
prcom |
|- { k , v } = { v , k } |
8 |
7
|
sseq1i |
|- ( { k , v } C_ e <-> { v , k } C_ e ) |
9 |
8
|
rexbii |
|- ( E. e e. E { k , v } C_ e <-> E. e e. E { v , k } C_ e ) |
10 |
|
id |
|- ( v e. V -> v e. V ) |
11 |
|
eldifi |
|- ( k e. ( V \ { v } ) -> k e. V ) |
12 |
10 11
|
anim12ci |
|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( k e. V /\ v e. V ) ) |
13 |
|
eldifsni |
|- ( k e. ( V \ { v } ) -> k =/= v ) |
14 |
13
|
adantl |
|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> k =/= v ) |
15 |
12 14
|
jca |
|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( ( k e. V /\ v e. V ) /\ k =/= v ) ) |
16 |
15
|
biantrurd |
|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( E. e e. E { v , k } C_ e <-> ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) ) ) |
17 |
9 16
|
bitr2id |
|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( ( ( ( k e. V /\ v e. V ) /\ k =/= v ) /\ E. e e. E { v , k } C_ e ) <-> E. e e. E { k , v } C_ e ) ) |
18 |
6 17
|
syl5bb |
|- ( ( v e. V /\ k e. ( V \ { v } ) ) -> ( k e. ( G NeighbVtx v ) <-> E. e e. E { k , v } C_ e ) ) |
19 |
18
|
ralbidva |
|- ( v e. V -> ( A. k e. ( V \ { v } ) k e. ( G NeighbVtx v ) <-> A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e ) ) |
20 |
19
|
rabbiia |
|- { v e. V | A. k e. ( V \ { v } ) k e. ( G NeighbVtx v ) } = { v e. V | A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e } |
21 |
3 20
|
eqtri |
|- ( UnivVtx ` G ) = { v e. V | A. k e. ( V \ { v } ) E. e e. E { k , v } C_ e } |