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

Definition df-ushgr 25725
 Description: Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function 𝑒 is an injective (one-to-one) function into subsets of the set of vertices 𝑣, representing the (one or more) vertices incident to the edge. This definition corresponds to definition of hypergraphs in section I.1 of [Bollobas] p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of [Diestel] p. 27, where "E is a subsets of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E are non-empty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.) (Revised by AV, 8-Oct-2020.)
Assertion
Ref Expression
df-ushgr USHGraph = {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})}
Distinct variable group:   𝑒,𝑔,𝑣

Detailed syntax breakdown of Definition df-ushgr
StepHypRef Expression
1 cushgr 25723 . 2 class USHGraph
2 ve . . . . . . . 8 setvar 𝑒
32cv 1474 . . . . . . 7 class 𝑒
43cdm 5038 . . . . . 6 class dom 𝑒
5 vv . . . . . . . . 9 setvar 𝑣
65cv 1474 . . . . . . . 8 class 𝑣
76cpw 4108 . . . . . . 7 class 𝒫 𝑣
8 c0 3874 . . . . . . . 8 class
98csn 4125 . . . . . . 7 class {∅}
107, 9cdif 3537 . . . . . 6 class (𝒫 𝑣 ∖ {∅})
114, 10, 3wf1 5801 . . . . 5 wff 𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})
12 vg . . . . . . 7 setvar 𝑔
1312cv 1474 . . . . . 6 class 𝑔
14 ciedg 25674 . . . . . 6 class iEdg
1513, 14cfv 5804 . . . . 5 class (iEdg‘𝑔)
1611, 2, 15wsbc 3402 . . . 4 wff [(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})
17 cvtx 25673 . . . . 5 class Vtx
1813, 17cfv 5804 . . . 4 class (Vtx‘𝑔)
1916, 5, 18wsbc 3402 . . 3 wff [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})
2019, 12cab 2596 . 2 class {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})}
211, 20wceq 1475 1 wff USHGraph = {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})}
 Colors of variables: wff setvar class This definition is referenced by:  isushgr  25727
 Copyright terms: Public domain W3C validator