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

Metamath Proof Explorer

Theorem uvtxnbgrb

Description: A vertex is universal iff all the other vertices are its neighbors. (Contributed by Alexander van der Vekens, 13-Jul-2018) (Revised by AV, 3-Nov-2020) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypothesis uvtxnbgr.v 
|- V = ( Vtx ` G )
Assertion uvtxnbgrb 
|- ( N e. V -> ( N e. ( UnivVtx ` G ) <-> ( G NeighbVtx N ) = ( V \ { N } ) ) )

Proof

Step Hyp Ref Expression
1 uvtxnbgr.v 
 |-  V = ( Vtx ` G )
2 1 uvtxnbgr 
 |-  ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) = ( V \ { N } ) )
3 simpl 
 |-  ( ( N e. V /\ ( G NeighbVtx N ) = ( V \ { N } ) ) -> N e. V )
4 raleleq 
 |-  ( ( V \ { N } ) = ( G NeighbVtx N ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) )
5 4 eqcoms 
 |-  ( ( G NeighbVtx N ) = ( V \ { N } ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) )
6 5 adantl 
 |-  ( ( N e. V /\ ( G NeighbVtx N ) = ( V \ { N } ) ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) )
7 1 uvtxel 
 |-  ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) )
8 3 6 7 sylanbrc 
 |-  ( ( N e. V /\ ( G NeighbVtx N ) = ( V \ { N } ) ) -> N e. ( UnivVtx ` G ) )
9 8 ex 
 |-  ( N e. V -> ( ( G NeighbVtx N ) = ( V \ { N } ) -> N e. ( UnivVtx ` G ) ) )
10 2 9 impbid2 
 |-  ( N e. V -> ( N e. ( UnivVtx ` G ) <-> ( G NeighbVtx N ) = ( V \ { N } ) ) )