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 FinUSGraph U V U UnivVtx G VtxDeg G U = V 1

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v V = Vtx G
2 1 uvtxnbvtxm1 G FinUSGraph U V U UnivVtx G G NeighbVtx U = V 1
3 fusgrusgr G FinUSGraph G USGraph
4 1 hashnbusgrvd G USGraph U V G NeighbVtx U = VtxDeg G U
5 3 4 sylan G FinUSGraph U V G NeighbVtx U = VtxDeg G U
6 5 eqeq1d G FinUSGraph U V G NeighbVtx U = V 1 VtxDeg G U = V 1
7 2 6 bitrd G FinUSGraph U V U UnivVtx G VtxDeg G U = V 1