Metamath Proof Explorer


Theorem vdiscusgrb

Description: A finite simple graph with n vertices is complete iff every vertex has degree n - 1 . (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 22-Dec-2020)

Ref Expression
Hypothesis hashnbusgrvd.v V = Vtx G
Assertion vdiscusgrb G FinUSGraph G ComplUSGraph v V VtxDeg G v = V 1

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v V = Vtx G
2 fusgrusgr G FinUSGraph G USGraph
3 1 cusgruvtxb G USGraph G ComplUSGraph UnivVtx G = V
4 1 uvtxssvtx UnivVtx G V
5 eqcom UnivVtx G = V V = UnivVtx G
6 sssseq UnivVtx G V V UnivVtx G V = UnivVtx G
7 5 6 bitr4id UnivVtx G V UnivVtx G = V V UnivVtx G
8 4 7 mp1i G USGraph UnivVtx G = V V UnivVtx G
9 3 8 bitrd G USGraph G ComplUSGraph V UnivVtx G
10 dfss3 V UnivVtx G v V v UnivVtx G
11 9 10 bitrdi G USGraph G ComplUSGraph v V v UnivVtx G
12 2 11 syl G FinUSGraph G ComplUSGraph v V v UnivVtx G
13 1 usgruvtxvdb G FinUSGraph v V v UnivVtx G VtxDeg G v = V 1
14 13 ralbidva G FinUSGraph v V v UnivVtx G v V VtxDeg G v = V 1
15 12 14 bitrd G FinUSGraph G ComplUSGraph v V VtxDeg G v = V 1