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