Metamath Proof Explorer

Theorem cusgrm1rusgr

Description: A finite simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGraph was allowed for k e. ZZ , then the assumption V =/= (/) could be removed. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Hypothesis cusgrrusgr.v 
|- V = ( Vtx ` G )
Assertion cusgrm1rusgr 
|- ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( G e. ComplUSGraph <-> G RegUSGraph ( ( # ` V ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 cusgrrusgr.v 
 |-  V = ( Vtx ` G )
2 simpr 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ G e. ComplUSGraph ) -> G e. ComplUSGraph )
3 1 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> V e. Fin )
4 3 adantr 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> V e. Fin )
5 4 adantr 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ G e. ComplUSGraph ) -> V e. Fin )
6 simpr 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> V =/= (/) )
7 6 adantr 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ G e. ComplUSGraph ) -> V =/= (/) )
8 1 cusgrrusgr 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> G RegUSGraph ( ( # ` V ) - 1 ) )
9 2 5 7 8 syl3anc 
 |-  ( ( ( G e. FinUSGraph /\ V =/= (/) ) /\ G e. ComplUSGraph ) -> G RegUSGraph ( ( # ` V ) - 1 ) )
10 9 ex 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( G e. ComplUSGraph -> G RegUSGraph ( ( # ` V ) - 1 ) ) )
11 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
12 1 11 rusgrprop0 
 |-  ( G RegUSGraph ( ( # ` V ) - 1 ) -> ( G e. USGraph /\ ( ( # ` V ) - 1 ) e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) )
13 12 simp3d 
 |-  ( G RegUSGraph ( ( # ` V ) - 1 ) -> A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) )
14 1 vdiscusgr 
 |-  ( G e. FinUSGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) -> G e. ComplUSGraph ) )
15 14 adantr 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) -> G e. ComplUSGraph ) )
16 13 15 syl5 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( G RegUSGraph ( ( # ` V ) - 1 ) -> G e. ComplUSGraph ) )
17 10 16 impbid 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( G e. ComplUSGraph <-> G RegUSGraph ( ( # ` V ) - 1 ) ) )