Metamath Proof Explorer

Theorem vdiscusgr

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

Ref Expression
Hypothesis hashnbusgrvd.v 
|- V = ( Vtx ` G )
Assertion vdiscusgr 
|- ( G e. FinUSGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) -> G e. ComplUSGraph ) )

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v 
 |-  V = ( Vtx ` G )
2 1 uvtxisvtx 
 |-  ( n e. ( UnivVtx ` G ) -> n e. V )
3 fveqeq2 
 |-  ( v = n -> ( ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) <-> ( ( VtxDeg ` G ) ` n ) = ( ( # ` V ) - 1 ) ) )
4 3 rspccv 
 |-  ( A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) -> ( n e. V -> ( ( VtxDeg ` G ) ` n ) = ( ( # ` V ) - 1 ) ) )
5 4 adantl 
 |-  ( ( G e. FinUSGraph /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) -> ( n e. V -> ( ( VtxDeg ` G ) ` n ) = ( ( # ` V ) - 1 ) ) )
6 5 imp 
 |-  ( ( ( G e. FinUSGraph /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) /\ n e. V ) -> ( ( VtxDeg ` G ) ` n ) = ( ( # ` V ) - 1 ) )
7 1 usgruvtxvdb 
 |-  ( ( G e. FinUSGraph /\ n e. V ) -> ( n e. ( UnivVtx ` G ) <-> ( ( VtxDeg ` G ) ` n ) = ( ( # ` V ) - 1 ) ) )
8 7 adantlr 
 |-  ( ( ( G e. FinUSGraph /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) /\ n e. V ) -> ( n e. ( UnivVtx ` G ) <-> ( ( VtxDeg ` G ) ` n ) = ( ( # ` V ) - 1 ) ) )
9 6 8 mpbird 
 |-  ( ( ( G e. FinUSGraph /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) /\ n e. V ) -> n e. ( UnivVtx ` G ) )
10 9 ex 
 |-  ( ( G e. FinUSGraph /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) -> ( n e. V -> n e. ( UnivVtx ` G ) ) )
11 2 10 impbid2 
 |-  ( ( G e. FinUSGraph /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) -> ( n e. ( UnivVtx ` G ) <-> n e. V ) )
12 11 eqrdv 
 |-  ( ( G e. FinUSGraph /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) -> ( UnivVtx ` G ) = V )
13 fusgrusgr 
 |-  ( G e. FinUSGraph -> G e. USGraph )
14 1 cusgruvtxb 
 |-  ( G e. USGraph -> ( G e. ComplUSGraph <-> ( UnivVtx ` G ) = V ) )
15 13 14 syl 
 |-  ( G e. FinUSGraph -> ( G e. ComplUSGraph <-> ( UnivVtx ` G ) = V ) )
16 15 adantr 
 |-  ( ( G e. FinUSGraph /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) -> ( G e. ComplUSGraph <-> ( UnivVtx ` G ) = V ) )
17 12 16 mpbird 
 |-  ( ( G e. FinUSGraph /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) -> G e. ComplUSGraph )
18 17 ex 
 |-  ( G e. FinUSGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) -> G e. ComplUSGraph ) )