Metamath Proof Explorer


Theorem nbusgrvtxm1uvtx

Description: If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, the vertex is universal. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 16-Dec-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypothesis uvtxnm1nbgr.v V=VtxG
Assertion nbusgrvtxm1uvtx GFinUSGraphUVGNeighbVtxU=V1UUnivVtxG

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v V=VtxG
2 1 nbgrssovtx GNeighbVtxUVU
3 2 sseli vGNeighbVtxUvVU
4 eldifsn vVUvVvU
5 1 nbusgrvtxm1 GFinUSGraphUVGNeighbVtxU=V1vVvUvGNeighbVtxU
6 5 imp GFinUSGraphUVGNeighbVtxU=V1vVvUvGNeighbVtxU
7 4 6 syl5bi GFinUSGraphUVGNeighbVtxU=V1vVUvGNeighbVtxU
8 3 7 impbid2 GFinUSGraphUVGNeighbVtxU=V1vGNeighbVtxUvVU
9 8 eqrdv GFinUSGraphUVGNeighbVtxU=V1GNeighbVtxU=VU
10 1 uvtxnbgrb UVUUnivVtxGGNeighbVtxU=VU
11 10 ad2antlr GFinUSGraphUVGNeighbVtxU=V1UUnivVtxGGNeighbVtxU=VU
12 9 11 mpbird GFinUSGraphUVGNeighbVtxU=V1UUnivVtxG
13 12 ex GFinUSGraphUVGNeighbVtxU=V1UUnivVtxG