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

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

Detailed syntax breakdown of Definition df-uhgr
StepHypRef Expression
1 cuhgr 32733 . 2  class UHGraph
2 ve . . . . . . . 8  setvar  e
32cv 1397 . . . . . . 7  class  e
43cdm 4988 . . . . . 6  class  dom  e
5 vv . . . . . . . . 9  setvar  v
65cv 1397 . . . . . . . 8  class  v
76cpw 3999 . . . . . . 7  class  ~P v
8 c0 3783 . . . . . . . 8  class  (/)
98csn 4016 . . . . . . 7  class  { (/) }
107, 9cdif 3458 . . . . . 6  class  ( ~P v  \  { (/) } )
114, 10, 3wf 5566 . . . . 5  wff  e : dom  e --> ( ~P v  \  { (/) } )
12 vg . . . . . . 7  setvar  g
1312cv 1397 . . . . . 6  class  g
14 cedgf 32732 . . . . . 6  class .ef
1513, 14cfv 5570 . . . . 5  class  ( .ef  `  g )
1611, 2, 15wsbc 3324 . . . 4  wff  [. ( .ef  `  g )  /  e ]. e : dom  e --> ( ~P v  \  { (/)
} )
17 cbs 14716 . . . . 5  class  Base
1813, 17cfv 5570 . . . 4  class  ( Base `  g )
1916, 5, 18wsbc 3324 . . 3  wff  [. ( Base `  g )  / 
v ]. [. ( .ef  `  g )  /  e ]. e : dom  e --> ( ~P v  \  { (/)
} )
2019, 12cab 2439 . 2  class  { g  |  [. ( Base `  g )  /  v ]. [. ( .ef  `  g
)  /  e ]. e : dom  e --> ( ~P v  \  { (/)
} ) }
211, 20wceq 1398 1  wff UHGraph  =  {
g  |  [. ( Base `  g )  / 
v ]. [. ( .ef  `  g )  /  e ]. e : dom  e --> ( ~P v  \  { (/)
} ) }
Colors of variables: wff setvar class
This definition is referenced by:  isuhgr  32738
  Copyright terms: Public domain W3C validator