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

Definition df-uhgr 27424
Description: Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into the power set 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 = {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})}
Distinct variable group:   𝑒,𝑔,𝑣

Detailed syntax breakdown of Definition df-uhgr
StepHypRef Expression
1 cuhgr 27422 . 2 class UHGraph
2 ve . . . . . . . 8 setvar 𝑒
32cv 1541 . . . . . . 7 class 𝑒
43cdm 5589 . . . . . 6 class dom 𝑒
5 vv . . . . . . . . 9 setvar 𝑣
65cv 1541 . . . . . . . 8 class 𝑣
76cpw 4539 . . . . . . 7 class 𝒫 𝑣
8 c0 4262 . . . . . . . 8 class
98csn 4567 . . . . . . 7 class {∅}
107, 9cdif 3889 . . . . . 6 class (𝒫 𝑣 ∖ {∅})
114, 10, 3wf 6427 . . . . 5 wff 𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})
12 vg . . . . . . 7 setvar 𝑔
1312cv 1541 . . . . . 6 class 𝑔
14 ciedg 27363 . . . . . 6 class iEdg
1513, 14cfv 6431 . . . . 5 class (iEdg‘𝑔)
1611, 2, 15wsbc 3720 . . . 4 wff [(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})
17 cvtx 27362 . . . . 5 class Vtx
1813, 17cfv 6431 . . . 4 class (Vtx‘𝑔)
1916, 5, 18wsbc 3720 . . 3 wff [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})
2019, 12cab 2717 . 2 class {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})}
211, 20wceq 1542 1 wff UHGraph = {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})}
Colors of variables: wff setvar class
This definition is referenced by:  isuhgr  27426
  Copyright terms: Public domain W3C validator