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 ) )