Description: A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 3-Nov-2020) (Revised by AV, 23-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | uvtxnbgr.v | |- V = ( Vtx ` G ) |
|
Assertion | uvtxnbgr | |- ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) = ( V \ { N } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uvtxnbgr.v | |- V = ( Vtx ` G ) |
|
2 | 1 | nbgrssovtx | |- ( G NeighbVtx N ) C_ ( V \ { N } ) |
3 | 2 | a1i | |- ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) C_ ( V \ { N } ) ) |
4 | 1 | uvtxnbgrss | |- ( N e. ( UnivVtx ` G ) -> ( V \ { N } ) C_ ( G NeighbVtx N ) ) |
5 | 3 4 | eqssd | |- ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) = ( V \ { N } ) ) |