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∈FinUSGraph→E≤(V2)

Proof

Step Hyp Ref Expression
1 fusgrmaxsize.v ⊢V=Vtx⁡G
2 fusgrmaxsize.e ⊢E=Edg⁡G
3 1 isfusgr ⊢G∈FinUSGraph↔G∈USGraph∧V∈Fin
4 cusgrexg ⊢V∈Fin→∃eVe∈ComplUSGraph
5 4 adantl ⊢G∈USGraph∧V∈Fin→∃eVe∈ComplUSGraph
6 1 fvexi ⊢V∈V
7 vex ⊢e∈V
8 6 7 opvtxfvi ⊢Vtx⁡Ve=V
9 8 eqcomi ⊢V=Vtx⁡Ve
10 eqid ⊢Edg⁡Ve=Edg⁡Ve
11 1 2 9 10 sizusglecusg ⊢G∈USGraph∧Ve∈ComplUSGraph→E≤Edg⁡Ve
12 11 adantlr ⊢G∈USGraph∧V∈Fin∧Ve∈ComplUSGraph→E≤Edg⁡Ve
13 9 10 cusgrsize ⊢Ve∈ComplUSGraph∧V∈Fin→Edg⁡Ve=(V2)
14 breq2 ⊢Edg⁡Ve=(V2)→E≤Edg⁡Ve↔E≤(V2)
15 14 biimpd ⊢Edg⁡Ve=(V2)→E≤Edg⁡Ve→E≤(V2)
16 13 15 syl ⊢Ve∈ComplUSGraph∧V∈Fin→E≤Edg⁡Ve→E≤(V2)
17 16 expcom ⊢V∈Fin→Ve∈ComplUSGraph→E≤Edg⁡Ve→E≤(V2)
18 17 adantl ⊢G∈USGraph∧V∈Fin→Ve∈ComplUSGraph→E≤Edg⁡Ve→E≤(V2)
19 18 imp ⊢G∈USGraph∧V∈Fin∧Ve∈ComplUSGraph→E≤Edg⁡Ve→E≤(V2)
20 12 19 mpd ⊢G∈USGraph∧V∈Fin∧Ve∈ComplUSGraph→E≤(V2)
21 5 20 exlimddv ⊢G∈USGraph∧V∈Fin→E≤(V2)
22 3 21 sylbi ⊢G∈FinUSGraph→E≤(V2)