This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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