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 ) ) )