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