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 ∖ k n k ∈ 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 ∖ k n ∈ G NeighbVtx k
5 2 nbusgreledg ⊢ G ∈ USGraph → n ∈ G NeighbVtx k ↔ n k ∈ E
6 5 2ralbidv ⊢ G ∈ USGraph → ∀ k ∈ V ∀ n ∈ V ∖ k n ∈ G NeighbVtx k ↔ ∀ k ∈ V ∀ n ∈ V ∖ k n k ∈ E
7 4 6 bitrd ⊢ G ∈ USGraph → G ∈ ComplGraph ↔ ∀ k ∈ V ∀ n ∈ V ∖ k n k ∈ E
8 7 pm5.32i ⊢ G ∈ USGraph ∧ G ∈ ComplGraph ↔ G ∈ USGraph ∧ ∀ k ∈ V ∀ n ∈ V ∖ k n k ∈ E
9 3 8 bitri ⊢ G ∈ ComplUSGraph ↔ G ∈ USGraph ∧ ∀ k ∈ V ∀ n ∈ V ∖ k n k ∈ E