Metamath Proof Explorer

Theorem iscplgrnb

Description: A graph is complete iff all vertices are neighbors of all vertices. (Contributed by AV, 1-Nov-2020)

Ref Expression
Hypothesis cplgruvtxb.v ⊢V=Vtx⁡G
Assertion iscplgrnb ⊢G∈W→G∈ComplGraph↔∀v∈V∀n∈V∖vn∈GNeighbVtxv

Proof

Step Hyp Ref Expression
1 cplgruvtxb.v ⊢V=Vtx⁡G
2 1 iscplgr ⊢G∈W→G∈ComplGraph↔∀v∈Vv∈UnivVtx⁡G
3 1 uvtxel ⊢v∈UnivVtx⁡G↔v∈V∧∀n∈V∖vn∈GNeighbVtxv
4 3 a1i ⊢G∈W→v∈UnivVtx⁡G↔v∈V∧∀n∈V∖vn∈GNeighbVtxv
5 4 baibd ⊢G∈W∧v∈V→v∈UnivVtx⁡G↔∀n∈V∖vn∈GNeighbVtxv
6 5 ralbidva ⊢G∈W→∀v∈Vv∈UnivVtx⁡G↔∀v∈V∀n∈V∖vn∈GNeighbVtxv
7 2 6 bitrd ⊢G∈W→G∈ComplGraph↔∀v∈V∀n∈V∖vn∈GNeighbVtxv