Metamath Proof Explorer

Theorem nbusgrvtxm1uvtx

Description: If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, the vertex is universal. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 16-Dec-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypothesis uvtxnm1nbgr.v 
|- V = ( Vtx ` G )
Assertion nbusgrvtxm1uvtx 
|- ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> U e. ( UnivVtx ` G ) ) )

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v 
 |-  V = ( Vtx ` G )
2 1 nbgrssovtx 
 |-  ( G NeighbVtx U ) C_ ( V \ { U } )
3 2 sseli 
 |-  ( v e. ( G NeighbVtx U ) -> v e. ( V \ { U } ) )
4 eldifsn 
 |-  ( v e. ( V \ { U } ) <-> ( v e. V /\ v =/= U ) )
5 1 nbusgrvtxm1 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> ( ( v e. V /\ v =/= U ) -> v e. ( G NeighbVtx U ) ) ) )
6 5 imp 
 |-  ( ( ( G e. FinUSGraph /\ U e. V ) /\ ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) -> ( ( v e. V /\ v =/= U ) -> v e. ( G NeighbVtx U ) ) )
7 4 6 syl5bi 
 |-  ( ( ( G e. FinUSGraph /\ U e. V ) /\ ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) -> ( v e. ( V \ { U } ) -> v e. ( G NeighbVtx U ) ) )
8 3 7 impbid2 
 |-  ( ( ( G e. FinUSGraph /\ U e. V ) /\ ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) -> ( v e. ( G NeighbVtx U ) <-> v e. ( V \ { U } ) ) )
9 8 eqrdv 
 |-  ( ( ( G e. FinUSGraph /\ U e. V ) /\ ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) -> ( G NeighbVtx U ) = ( V \ { U } ) )
10 1 uvtxnbgrb 
 |-  ( U e. V -> ( U e. ( UnivVtx ` G ) <-> ( G NeighbVtx U ) = ( V \ { U } ) ) )
11 10 ad2antlr 
 |-  ( ( ( G e. FinUSGraph /\ U e. V ) /\ ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) -> ( U e. ( UnivVtx ` G ) <-> ( G NeighbVtx U ) = ( V \ { U } ) ) )
12 9 11 mpbird 
 |-  ( ( ( G e. FinUSGraph /\ U e. V ) /\ ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) -> U e. ( UnivVtx ` G ) )
13 12 ex 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) -> U e. ( UnivVtx ` G ) ) )