Metamath Proof Explorer

Theorem iscplgredg

Description: A graph G is complete iff all vertices are connected with each other by (at least) one edge. (Contributed by AV, 10-Nov-2020)

Ref Expression
Hypotheses cplgruvtxb.v ⊢V=Vtx⁡G
iscplgredg.v ⊢E=Edg⁡G
Assertion iscplgredg ⊢G∈W→G∈ComplGraph↔∀v∈V∀n∈V∖v∃e∈Evn⊆e

Proof

Step Hyp Ref Expression
1 cplgruvtxb.v ⊢V=Vtx⁡G
2 iscplgredg.v ⊢E=Edg⁡G
3 1 iscplgrnb ⊢G∈W→G∈ComplGraph↔∀v∈V∀n∈V∖vn∈GNeighbVtxv
4 df-3an ⊢n∈V∧v∈V∧n≠v∧∃e∈Evn⊆e↔n∈V∧v∈V∧n≠v∧∃e∈Evn⊆e
5 4 a1i ⊢G∈W∧v∈V∧n∈V∖v→n∈V∧v∈V∧n≠v∧∃e∈Evn⊆e↔n∈V∧v∈V∧n≠v∧∃e∈Evn⊆e
6 1 2 nbgrel ⊢n∈GNeighbVtxv↔n∈V∧v∈V∧n≠v∧∃e∈Evn⊆e
7 6 a1i ⊢G∈W∧v∈V∧n∈V∖v→n∈GNeighbVtxv↔n∈V∧v∈V∧n≠v∧∃e∈Evn⊆e
8 eldifsn ⊢n∈V∖v↔n∈V∧n≠v
9 simpr ⊢G∈W∧v∈V→v∈V
10 simpl ⊢n∈V∧n≠v→n∈V
11 9 10 anim12ci ⊢G∈W∧v∈V∧n∈V∧n≠v→n∈V∧v∈V
12 simprr ⊢G∈W∧v∈V∧n∈V∧n≠v→n≠v
13 11 12 jca ⊢G∈W∧v∈V∧n∈V∧n≠v→n∈V∧v∈V∧n≠v
14 8 13 sylan2b ⊢G∈W∧v∈V∧n∈V∖v→n∈V∧v∈V∧n≠v
15 14 biantrurd ⊢G∈W∧v∈V∧n∈V∖v→∃e∈Evn⊆e↔n∈V∧v∈V∧n≠v∧∃e∈Evn⊆e
16 5 7 15 3bitr4d ⊢G∈W∧v∈V∧n∈V∖v→n∈GNeighbVtxv↔∃e∈Evn⊆e
17 16 ralbidva ⊢G∈W∧v∈V→∀n∈V∖vn∈GNeighbVtxv↔∀n∈V∖v∃e∈Evn⊆e
18 17 ralbidva ⊢G∈W→∀v∈V∀n∈V∖vn∈GNeighbVtxv↔∀v∈V∀n∈V∖v∃e∈Evn⊆e
19 3 18 bitrd ⊢G∈W→G∈ComplGraph↔∀v∈V∀n∈V∖v∃e∈Evn⊆e