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

Definition df-uhgr 39246
Description: Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set 
v (of "vertices") and a function  e (representing indexed "edges") into the powerset of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 8-Oct-2020.)
Assertion
Ref Expression
df-uhgr  |- UHGraph  =  {
g  |  [. (Vtx `  g )  /  v ]. [. (iEdg `  g
)  /  e ]. e : dom  e --> ( ~P v  \  { (/)
} ) }
Distinct variable group:    e, g, v

Detailed syntax breakdown of Definition df-uhgr
StepHypRef Expression
1 cuhgr 39244 . 2  class UHGraph
2 ve . . . . . . . 8  setvar  e
32cv 1446 . . . . . . 7  class  e
43cdm 4811 . . . . . 6  class  dom  e
5 vv . . . . . . . . 9  setvar  v
65cv 1446 . . . . . . . 8  class  v
76cpw 3918 . . . . . . 7  class  ~P v
8 c0 3698 . . . . . . . 8  class  (/)
98csn 3935 . . . . . . 7  class  { (/) }
107, 9cdif 3368 . . . . . 6  class  ( ~P v  \  { (/) } )
114, 10, 3wf 5556 . . . . 5  wff  e : dom  e --> ( ~P v  \  { (/) } )
12 vg . . . . . . 7  setvar  g
1312cv 1446 . . . . . 6  class  g
14 ciedg 39199 . . . . . 6  class iEdg
1513, 14cfv 5560 . . . . 5  class  (iEdg `  g )
1611, 2, 15wsbc 3234 . . . 4  wff  [. (iEdg `  g )  /  e ]. e : dom  e --> ( ~P v  \  { (/)
} )
17 cvtx 39198 . . . . 5  class Vtx
1813, 17cfv 5560 . . . 4  class  (Vtx `  g )
1916, 5, 18wsbc 3234 . . 3  wff  [. (Vtx `  g )  /  v ]. [. (iEdg `  g
)  /  e ]. e : dom  e --> ( ~P v  \  { (/)
} )
2019, 12cab 2437 . 2  class  { g  |  [. (Vtx `  g )  /  v ]. [. (iEdg `  g
)  /  e ]. e : dom  e --> ( ~P v  \  { (/)
} ) }
211, 20wceq 1447 1  wff UHGraph  =  {
g  |  [. (Vtx `  g )  /  v ]. [. (iEdg `  g
)  /  e ]. e : dom  e --> ( ~P v  \  { (/)
} ) }
Colors of variables: wff setvar class
This definition is referenced by:  isuhgr  39248
  Copyright terms: Public domain W3C validator