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

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion usgruvtxvdb ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 uvtxnbvtxm1 ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
3 fusgrusgr ⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
4 1 hashnbusgrvd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) )
5 3 4 sylan ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) )
6 5 eqeq1d ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
7 2 6 bitrd ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )