Theorem uvtxnbvtxm1

Description: A universal vertex has n - 1 neighbors in a finite simple graph with n vertices. A biconditional version of nbusgrvtxm1uvtx resp. uvtxnm1nbgr . (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 16-Dec-2020)

	Ref	Expression
Hypothesis	uvtxnm1nbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	uvtxnbvtxm1	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		uvtxnm1nbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	uvtxnm1nbgr	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
3	2	ex	⊢ ( 𝐺 ∈ FinUSGraph → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
4	3	adantr	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
5	1	nbusgrvtxm1uvtx	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ) )
6	4 5	impbid	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )