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 ≤ ( V 2 )

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 → ∃ e V e ∈ ComplUSGraph
5 4 adantl ⊢ G ∈ USGraph ∧ V ∈ Fin → ∃ e V e ∈ ComplUSGraph
6 1 fvexi ⊢ V ∈ V
7 vex ⊢ 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 ∈ USGraph ∧ V e ∈ ComplUSGraph → E ≤ Edg ⁡ V e
12 11 adantlr ⊢ G ∈ USGraph ∧ V ∈ Fin ∧ V e ∈ ComplUSGraph → E ≤ Edg ⁡ V e
13 9 10 cusgrsize ⊢ V e ∈ ComplUSGraph ∧ V ∈ Fin → Edg ⁡ V e = ( V 2 )
14 breq2 ⊢ Edg ⁡ V e = ( V 2 ) → E ≤ Edg ⁡ V e ↔ E ≤ ( V 2 )
15 14 biimpd ⊢ Edg ⁡ V e = ( V 2 ) → E ≤ Edg ⁡ V e → E ≤ ( V 2 )
16 13 15 syl ⊢ V e ∈ ComplUSGraph ∧ V ∈ Fin → E ≤ Edg ⁡ V e → E ≤ ( V 2 )
17 16 expcom ⊢ V ∈ Fin → V e ∈ ComplUSGraph → E ≤ Edg ⁡ V e → E ≤ ( V 2 )
18 17 adantl ⊢ G ∈ USGraph ∧ V ∈ Fin → V e ∈ ComplUSGraph → E ≤ Edg ⁡ V e → E ≤ ( V 2 )
19 18 imp ⊢ G ∈ USGraph ∧ V ∈ Fin ∧ V e ∈ ComplUSGraph → E ≤ Edg ⁡ V e → E ≤ ( V 2 )
20 12 19 mpd ⊢ G ∈ USGraph ∧ V ∈ Fin ∧ V e ∈ ComplUSGraph → E ≤ ( V 2 )
21 5 20 exlimddv ⊢ G ∈ USGraph ∧ V ∈ Fin → E ≤ ( V 2 )
22 3 21 sylbi ⊢ G ∈ FinUSGraph → E ≤ ( V 2 )