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

Definition df-ushgr 28299
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 the 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 subset of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty 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 28297 . 2 class USHGraph
2 ve . . . . . . . 8 setvar 𝑒
32cv 1541 . . . . . . 7 class 𝑒
43cdm 5675 . . . . . 6 class dom 𝑒
5 vv . . . . . . . . 9 setvar 𝑣
65cv 1541 . . . . . . . 8 class 𝑣
76cpw 4601 . . . . . . 7 class 𝒫 𝑣
8 c0 4321 . . . . . . . 8 class
98csn 4627 . . . . . . 7 class {∅}
107, 9cdif 3944 . . . . . 6 class (𝒫 𝑣 ∖ {∅})
114, 10, 3wf1 6537 . . . . 5 wff 𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})
12 vg . . . . . . 7 setvar 𝑔
1312cv 1541 . . . . . 6 class 𝑔
14 ciedg 28237 . . . . . 6 class iEdg
1513, 14cfv 6540 . . . . 5 class (iEdg‘𝑔)
1611, 2, 15wsbc 3776 . . . 4 wff [(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})
17 cvtx 28236 . . . . 5 class Vtx
1813, 17cfv 6540 . . . 4 class (Vtx‘𝑔)
1916, 5, 18wsbc 3776 . . 3 wff [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})
2019, 12cab 2710 . 2 class {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})}
211, 20wceq 1542 1 wff USHGraph = {𝑔[(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})}
Colors of variables: wff setvar class
This definition is referenced by:  isushgr  28301
  Copyright terms: Public domain W3C validator