Metamath Proof Explorer

Theorem uvtxnm1nbgr

Description: A universal vertex has n - 1 neighbors in a finite graph with n vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 3-Nov-2020)

Ref Expression
Hypothesis uvtxnm1nbgr.v ⊢V=Vtx⁡G
Assertion uvtxnm1nbgr ⊢G∈FinUSGraph∧N∈UnivVtx⁡G→GNeighbVtxN=V−1

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v ⊢V=Vtx⁡G
2 1 uvtxnbgr ⊢N∈UnivVtx⁡G→GNeighbVtxN=V∖N
3 2 adantl ⊢G∈FinUSGraph∧N∈UnivVtx⁡G→GNeighbVtxN=V∖N
4 3 fveq2d ⊢G∈FinUSGraph∧N∈UnivVtx⁡G→GNeighbVtxN=V∖N
5 1 fusgrvtxfi ⊢G∈FinUSGraph→V∈Fin
6 1 uvtxisvtx ⊢N∈UnivVtx⁡G→N∈V
7 6 snssd ⊢N∈UnivVtx⁡G→N⊆V
8 hashssdif ⊢V∈Fin∧N⊆V→V∖N=V−N
9 5 7 8 syl2an ⊢G∈FinUSGraph∧N∈UnivVtx⁡G→V∖N=V−N
10 hashsng ⊢N∈UnivVtx⁡G→N=1
11 10 adantl ⊢G∈FinUSGraph∧N∈UnivVtx⁡G→N=1
12 11 oveq2d ⊢G∈FinUSGraph∧N∈UnivVtx⁡G→V−N=V−1
13 4 9 12 3eqtrd ⊢G∈FinUSGraph∧N∈UnivVtx⁡G→GNeighbVtxN=V−1