MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cusgra Structured version   Unicode version

Definition df-cusgra 23158
Description: Define the class of all complete (undirected simple) graphs. An undirected simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
Assertion
Ref Expression
df-cusgra  |- ComplUSGrph  =  { <. v ,  e >.  |  ( v USGrph  e  /\  A. k  e.  v 
A. n  e.  ( v  \  { k } ) { n ,  k }  e.  ran  e ) }
Distinct variable group:    v, e, k, n

Detailed syntax breakdown of Definition df-cusgra
StepHypRef Expression
1 ccusgra 23155 . 2  class ComplUSGrph
2 vv . . . . . 6  setvar  v
32cv 1363 . . . . 5  class  v
4 ve . . . . . 6  setvar  e
54cv 1363 . . . . 5  class  e
6 cusg 23089 . . . . 5  class USGrph
73, 5, 6wbr 4282 . . . 4  wff  v USGrph  e
8 vn . . . . . . . . 9  setvar  n
98cv 1363 . . . . . . . 8  class  n
10 vk . . . . . . . . 9  setvar  k
1110cv 1363 . . . . . . . 8  class  k
129, 11cpr 3869 . . . . . . 7  class  { n ,  k }
135crn 4830 . . . . . . 7  class  ran  e
1412, 13wcel 1757 . . . . . 6  wff  { n ,  k }  e.  ran  e
1511csn 3867 . . . . . . 7  class  { k }
163, 15cdif 3315 . . . . . 6  class  ( v 
\  { k } )
1714, 8, 16wral 2707 . . . . 5  wff  A. n  e.  ( v  \  {
k } ) { n ,  k }  e.  ran  e
1817, 10, 3wral 2707 . . . 4  wff  A. k  e.  v  A. n  e.  ( v  \  {
k } ) { n ,  k }  e.  ran  e
197, 18wa 369 . . 3  wff  ( v USGrph 
e  /\  A. k  e.  v  A. n  e.  ( v  \  {
k } ) { n ,  k }  e.  ran  e )
2019, 2, 4copab 4339 . 2  class  { <. v ,  e >.  |  ( v USGrph  e  /\  A. k  e.  v  A. n  e.  ( v  \  { k } ) { n ,  k }  e.  ran  e
) }
211, 20wceq 1364 1  wff ComplUSGrph  =  { <. v ,  e >.  |  ( v USGrph  e  /\  A. k  e.  v 
A. n  e.  ( v  \  { k } ) { n ,  k }  e.  ran  e ) }
Colors of variables: wff setvar class
This definition is referenced by:  iscusgra  23189  iscusgra0  23190  cusgrasize  23211
  Copyright terms: Public domain W3C validator