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 = Vtx G
Assertion nbusgrvtxm1uvtx G FinUSGraph U V G NeighbVtx U = V 1 U UnivVtx G

Proof

Step Hyp Ref Expression
1 uvtxnm1nbgr.v V = Vtx G
2 1 nbgrssovtx G NeighbVtx U V U
3 2 sseli v G NeighbVtx U v V U
4 eldifsn v V U v V v U
5 1 nbusgrvtxm1 G FinUSGraph U V G NeighbVtx U = V 1 v V v U v G NeighbVtx U
6 5 imp G FinUSGraph U V G NeighbVtx U = V 1 v V v U v G NeighbVtx U
7 4 6 syl5bi G FinUSGraph U V G NeighbVtx U = V 1 v V U v G NeighbVtx U
8 3 7 impbid2 G FinUSGraph U V G NeighbVtx U = V 1 v G NeighbVtx U v V U
9 8 eqrdv G FinUSGraph U V G NeighbVtx U = V 1 G NeighbVtx U = V U
10 1 uvtxnbgrb U V U UnivVtx G G NeighbVtx U = V U
11 10 ad2antlr G FinUSGraph U V G NeighbVtx U = V 1 U UnivVtx G G NeighbVtx U = V U
12 9 11 mpbird G FinUSGraph U V G NeighbVtx U = V 1 U UnivVtx G
13 12 ex G FinUSGraph U V G NeighbVtx U = V 1 U UnivVtx G