Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cplgr Structured version   Visualization version   GIF version

Definition df-cplgr 40557
 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. (Contributed by AV, 24-Oct-2020.)
Assertion
Ref Expression
df-cplgr ComplGraph = {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)𝑣 ∈ (UnivVtx‘𝑔)}
Distinct variable group:   𝑣,𝑔

Detailed syntax breakdown of Definition df-cplgr
StepHypRef Expression
1 ccplgr 40552 . 2 class ComplGraph
2 vv . . . . . 6 setvar 𝑣
32cv 1474 . . . . 5 class 𝑣
4 vg . . . . . . 7 setvar 𝑔
54cv 1474 . . . . . 6 class 𝑔
6 cuvtxa 40551 . . . . . 6 class UnivVtx
75, 6cfv 5804 . . . . 5 class (UnivVtx‘𝑔)
83, 7wcel 1977 . . . 4 wff 𝑣 ∈ (UnivVtx‘𝑔)
9 cvtx 25673 . . . . 5 class Vtx
105, 9cfv 5804 . . . 4 class (Vtx‘𝑔)
118, 2, 10wral 2896 . . 3 wff 𝑣 ∈ (Vtx‘𝑔)𝑣 ∈ (UnivVtx‘𝑔)
1211, 4cab 2596 . 2 class {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)𝑣 ∈ (UnivVtx‘𝑔)}
131, 12wceq 1475 1 wff ComplGraph = {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)𝑣 ∈ (UnivVtx‘𝑔)}
 Colors of variables: wff setvar class This definition is referenced by:  iscplgr  40636
 Copyright terms: Public domain W3C validator