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 𝑉 = ( Vtx ‘ 𝐺 )
fusgrmaxsize.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion fusgrmaxsize ( 𝐺 ∈ FinUSGraph → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) )

Proof

Step Hyp Ref Expression
1 fusgrmaxsize.v 𝑉 = ( Vtx ‘ 𝐺 )
2 fusgrmaxsize.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 isfusgr ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
4 cusgrexg ( 𝑉 ∈ Fin → ∃ 𝑒𝑉 , 𝑒 ⟩ ∈ ComplUSGraph )
5 4 adantl ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) → ∃ 𝑒𝑉 , 𝑒 ⟩ ∈ ComplUSGraph )
6 1 fvexi 𝑉 ∈ V
7 vex 𝑒 ∈ V
8 6 7 opvtxfvi ( Vtx ‘ ⟨ 𝑉 , 𝑒 ⟩ ) = 𝑉
9 8 eqcomi 𝑉 = ( Vtx ‘ ⟨ 𝑉 , 𝑒 ⟩ )
10 eqid ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) = ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ )
11 1 2 9 10 sizusglecusg ( ( 𝐺 ∈ USGraph ∧ ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) )
12 11 adantlr ( ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ∧ ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) )
13 9 10 cusgrsize ( ( ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )
14 breq2 ( ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) ↔ ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) )
15 14 biimpd ( ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) = ( ( ♯ ‘ 𝑉 ) C 2 ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) )
16 13 15 syl ( ( ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) )
17 16 expcom ( 𝑉 ∈ Fin → ( ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
18 17 adantl ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) → ( ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) ) )
19 18 imp ( ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ∧ ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph ) → ( ( ♯ ‘ 𝐸 ) ≤ ( ♯ ‘ ( Edg ‘ ⟨ 𝑉 , 𝑒 ⟩ ) ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) ) )
20 12 19 mpd ( ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ∧ ⟨ 𝑉 , 𝑒 ⟩ ∈ ComplUSGraph ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) )
21 5 20 exlimddv ( ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) )
22 3 21 sylbi ( 𝐺 ∈ FinUSGraph → ( ♯ ‘ 𝐸 ) ≤ ( ( ♯ ‘ 𝑉 ) C 2 ) )