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 e. FinUSGraph -> ( G e. ComplUSGraph <-> A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v 
 |-  V = ( Vtx ` G )
2 fusgrusgr 
 |-  ( G e. FinUSGraph -> G e. USGraph )
3 1 cusgruvtxb 
 |-  ( G e. USGraph -> ( G e. ComplUSGraph <-> ( UnivVtx ` G ) = V ) )
4 1 uvtxssvtx 
 |-  ( UnivVtx ` G ) C_ V
5 eqcom 
 |-  ( ( UnivVtx ` G ) = V <-> V = ( UnivVtx ` G ) )
6 sssseq 
 |-  ( ( UnivVtx ` G ) C_ V -> ( V C_ ( UnivVtx ` G ) <-> V = ( UnivVtx ` G ) ) )
7 5 6 bitr4id 
 |-  ( ( UnivVtx ` G ) C_ V -> ( ( UnivVtx ` G ) = V <-> V C_ ( UnivVtx ` G ) ) )
8 4 7 mp1i 
 |-  ( G e. USGraph -> ( ( UnivVtx ` G ) = V <-> V C_ ( UnivVtx ` G ) ) )
9 3 8 bitrd 
 |-  ( G e. USGraph -> ( G e. ComplUSGraph <-> V C_ ( UnivVtx ` G ) ) )
10 dfss3 
 |-  ( V C_ ( UnivVtx ` G ) <-> A. v e. V v e. ( UnivVtx ` G ) )
11 9 10 bitrdi 
 |-  ( G e. USGraph -> ( G e. ComplUSGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )
12 2 11 syl 
 |-  ( G e. FinUSGraph -> ( G e. ComplUSGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )
13 1 usgruvtxvdb 
 |-  ( ( G e. FinUSGraph /\ v e. V ) -> ( v e. ( UnivVtx ` G ) <-> ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) )
14 13 ralbidva 
 |-  ( G e. FinUSGraph -> ( A. v e. V v e. ( UnivVtx ` G ) <-> A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) )
15 12 14 bitrd 
 |-  ( G e. FinUSGraph -> ( G e. ComplUSGraph <-> A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) )