Metamath Proof Explorer

Theorem iscusgredg

Description: A simple graph is complete iff all vertices are connected by an edge. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 1-Nov-2020)

Ref Expression
Hypotheses iscusgrvtx.v ⊢V=Vtx⁡G
iscusgredg.v ⊢E=Edg⁡G
Assertion iscusgredg ⊢G∈ComplUSGraph↔G∈USGraph∧∀k∈V∀n∈V∖knk∈E

Proof

Step Hyp Ref Expression
1 iscusgrvtx.v ⊢V=Vtx⁡G
2 iscusgredg.v ⊢E=Edg⁡G
3 iscusgr ⊢G∈ComplUSGraph↔G∈USGraph∧G∈ComplGraph
4 1 iscplgrnb ⊢G∈USGraph→G∈ComplGraph↔∀k∈V∀n∈V∖kn∈GNeighbVtxk
5 2 nbusgreledg ⊢G∈USGraph→n∈GNeighbVtxk↔nk∈E
6 5 2ralbidv ⊢G∈USGraph→∀k∈V∀n∈V∖kn∈GNeighbVtxk↔∀k∈V∀n∈V∖knk∈E
7 4 6 bitrd ⊢G∈USGraph→G∈ComplGraph↔∀k∈V∀n∈V∖knk∈E
8 7 pm5.32i ⊢G∈USGraph∧G∈ComplGraph↔G∈USGraph∧∀k∈V∀n∈V∖knk∈E
9 3 8 bitri ⊢G∈ComplUSGraph↔G∈USGraph∧∀k∈V∀n∈V∖knk∈E