Metamath Proof Explorer

Theorem fusgrmaxsize

Description: The maximum size of a finite simple graph with n vertices is ( ( ( n - 1 ) * n ) / 2 ) . See statement in section I.1 of Bollobas p. 3 . (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 14-Nov-2020)

Ref Expression
Hypotheses fusgrmaxsize.v 
|- V = ( Vtx ` G )
fusgrmaxsize.e 
|- E = ( Edg ` G )
Assertion fusgrmaxsize 
|- ( G e. FinUSGraph -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) )

Proof

Step Hyp Ref Expression
1 fusgrmaxsize.v 
 |-  V = ( Vtx ` G )
2 fusgrmaxsize.e 
 |-  E = ( Edg ` G )
3 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
4 cusgrexg 
 |-  ( V e. Fin -> E. e <. V , e >. e. ComplUSGraph )
5 4 adantl 
 |-  ( ( G e. USGraph /\ V e. Fin ) -> E. e <. V , e >. e. ComplUSGraph )
6 1 fvexi 
 |-  V e. _V
7 vex 
 |-  e e. _V
8 6 7 opvtxfvi 
 |-  ( Vtx ` <. V , e >. ) = V
9 8 eqcomi 
 |-  V = ( Vtx ` <. V , e >. )
10 eqid 
 |-  ( Edg ` <. V , e >. ) = ( Edg ` <. V , e >. )
11 1 2 9 10 sizusglecusg 
 |-  ( ( G e. USGraph /\ <. V , e >. e. ComplUSGraph ) -> ( # ` E ) <_ ( # ` ( Edg ` <. V , e >. ) ) )
12 11 adantlr 
 |-  ( ( ( G e. USGraph /\ V e. Fin ) /\ <. V , e >. e. ComplUSGraph ) -> ( # ` E ) <_ ( # ` ( Edg ` <. V , e >. ) ) )
13 9 10 cusgrsize 
 |-  ( ( <. V , e >. e. ComplUSGraph /\ V e. Fin ) -> ( # ` ( Edg ` <. V , e >. ) ) = ( ( # ` V ) _C 2 ) )
14 breq2 
 |-  ( ( # ` ( Edg ` <. V , e >. ) ) = ( ( # ` V ) _C 2 ) -> ( ( # ` E ) <_ ( # ` ( Edg ` <. V , e >. ) ) <-> ( # ` E ) <_ ( ( # ` V ) _C 2 ) ) )
15 14 biimpd 
 |-  ( ( # ` ( Edg ` <. V , e >. ) ) = ( ( # ` V ) _C 2 ) -> ( ( # ` E ) <_ ( # ` ( Edg ` <. V , e >. ) ) -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) ) )
16 13 15 syl 
 |-  ( ( <. V , e >. e. ComplUSGraph /\ V e. Fin ) -> ( ( # ` E ) <_ ( # ` ( Edg ` <. V , e >. ) ) -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) ) )
17 16 expcom 
 |-  ( V e. Fin -> ( <. V , e >. e. ComplUSGraph -> ( ( # ` E ) <_ ( # ` ( Edg ` <. V , e >. ) ) -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) ) ) )
18 17 adantl 
 |-  ( ( G e. USGraph /\ V e. Fin ) -> ( <. V , e >. e. ComplUSGraph -> ( ( # ` E ) <_ ( # ` ( Edg ` <. V , e >. ) ) -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) ) ) )
19 18 imp 
 |-  ( ( ( G e. USGraph /\ V e. Fin ) /\ <. V , e >. e. ComplUSGraph ) -> ( ( # ` E ) <_ ( # ` ( Edg ` <. V , e >. ) ) -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) ) )
20 12 19 mpd 
 |-  ( ( ( G e. USGraph /\ V e. Fin ) /\ <. V , e >. e. ComplUSGraph ) -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) )
21 5 20 exlimddv 
 |-  ( ( G e. USGraph /\ V e. Fin ) -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) )
22 3 21 sylbi 
 |-  ( G e. FinUSGraph -> ( # ` E ) <_ ( ( # ` V ) _C 2 ) )