MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cplgr Structured version   Visualization version   GIF version

Definition df-cplgr 27192
Description: Define the class of all complete "graphs". A class/graph is called complete if every pair of distinct vertices is connected by an edge, i.e., each vertex has all other vertices as neighbors or, in other words, each vertex is a universal vertex. (Contributed by AV, 24-Oct-2020.) (Revised by TA, 15-Feb-2022.)
Assertion
Ref Expression
df-cplgr ComplGraph = {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)}

Detailed syntax breakdown of Definition df-cplgr
StepHypRef Expression
1 ccplgr 27190 . 2 class ComplGraph
2 vg . . . . . 6 setvar 𝑔
32cv 1532 . . . . 5 class 𝑔
4 cuvtx 27166 . . . . 5 class UnivVtx
53, 4cfv 6354 . . . 4 class (UnivVtx‘𝑔)
6 cvtx 26780 . . . . 5 class Vtx
73, 6cfv 6354 . . . 4 class (Vtx‘𝑔)
85, 7wceq 1533 . . 3 wff (UnivVtx‘𝑔) = (Vtx‘𝑔)
98, 2cab 2799 . 2 class {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)}
101, 9wceq 1533 1 wff ComplGraph = {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)}
Colors of variables: wff setvar class
This definition is referenced by:  cplgruvtxb  27194
  Copyright terms: Public domain W3C validator