Theorem uvtxnbgrss

Description: A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 30-Oct-2020)

	Ref	Expression
Hypothesis	uvtxel.v	|- V = ( Vtx ` G )
Assertion	uvtxnbgrss	|- ( N e. ( UnivVtx ` G ) -> ( V \ { N } ) C_ ( G NeighbVtx N ) )

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	|- V = ( Vtx ` G )
2	1	vtxnbuvtx	|- ( N e. ( UnivVtx ` G ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) )
3		dfss3	|- ( ( V \ { N } ) C_ ( G NeighbVtx N ) <-> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) )
4	2 3	sylibr	|- ( N e. ( UnivVtx ` G ) -> ( V \ { N } ) C_ ( G NeighbVtx N ) )