Metamath Proof Explorer

Theorem usgruvtxvdb

Description: In a finite simple graph with n vertices a vertex is universal iff the vertex has degree n - 1 . (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 17-Dec-2020)

Ref Expression
Hypothesis hashnbusgrvd.v 
|- V = ( Vtx ` G )
Assertion usgruvtxvdb 
|- ( ( G e. FinUSGraph /\ U e. V ) -> ( U e. ( UnivVtx ` G ) <-> ( ( VtxDeg ` G ) ` U ) = ( ( # ` V ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v 
 |-  V = ( Vtx ` G )
2 1 uvtxnbvtxm1 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( U e. ( UnivVtx ` G ) <-> ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) ) )
3 fusgrusgr 
 |-  ( G e. FinUSGraph -> G e. USGraph )
4 1 hashnbusgrvd 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( ( VtxDeg ` G ) ` U ) )
5 3 4 sylan 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( ( VtxDeg ` G ) ` U ) )
6 5 eqeq1d 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( ( # ` ( G NeighbVtx U ) ) = ( ( # ` V ) - 1 ) <-> ( ( VtxDeg ` G ) ` U ) = ( ( # ` V ) - 1 ) ) )
7 2 6 bitrd 
 |-  ( ( G e. FinUSGraph /\ U e. V ) -> ( U e. ( UnivVtx ` G ) <-> ( ( VtxDeg ` G ) ` U ) = ( ( # ` V ) - 1 ) ) )