Theorem uvtxnbgrvtx

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

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

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		eleq1w	|- ( n = v -> ( n e. ( G NeighbVtx N ) <-> v e. ( G NeighbVtx N ) ) )
4	3	rspcva	|- ( ( v e. ( V \ { N } ) /\ A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) -> v e. ( G NeighbVtx N ) )
5		nbgrsym	|- ( v e. ( G NeighbVtx N ) <-> N e. ( G NeighbVtx v ) )
6	5	a1i	|- ( N e. ( UnivVtx ` G ) -> ( v e. ( G NeighbVtx N ) <-> N e. ( G NeighbVtx v ) ) )
7	4 6	syl5ibcom	|- ( ( v e. ( V \ { N } ) /\ A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) -> ( N e. ( UnivVtx ` G ) -> N e. ( G NeighbVtx v ) ) )
8	7	expcom	|- ( A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) -> ( v e. ( V \ { N } ) -> ( N e. ( UnivVtx ` G ) -> N e. ( G NeighbVtx v ) ) ) )
9	8	com23	|- ( A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) -> ( N e. ( UnivVtx ` G ) -> ( v e. ( V \ { N } ) -> N e. ( G NeighbVtx v ) ) ) )
10	2 9	mpcom	|- ( N e. ( UnivVtx ` G ) -> ( v e. ( V \ { N } ) -> N e. ( G NeighbVtx v ) ) )
11	10	ralrimiv	|- ( N e. ( UnivVtx ` G ) -> A. v e. ( V \ { N } ) N e. ( G NeighbVtx v ) )