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

Definition df-ushgra 25822
 Description: Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a pair of a set and an injective (one-to-one) function into the powerset of this set (the empty set excluded). (Contributed by AV, 19-Jan-2020.)
Assertion
Ref Expression
df-ushgra USHGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})}
Distinct variable group:   𝑣,𝑒

Detailed syntax breakdown of Definition df-ushgra
StepHypRef Expression
1 cushg 25820 . 2 class USHGrph
2 ve . . . . . 6 setvar 𝑒
32cv 1474 . . . . 5 class 𝑒
43cdm 5038 . . . 4 class dom 𝑒
5 vv . . . . . . 7 setvar 𝑣
65cv 1474 . . . . . 6 class 𝑣
76cpw 4108 . . . . 5 class 𝒫 𝑣
8 c0 3874 . . . . . 6 class
98csn 4125 . . . . 5 class {∅}
107, 9cdif 3537 . . . 4 class (𝒫 𝑣 ∖ {∅})
114, 10, 3wf1 5801 . . 3 wff 𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})
1211, 5, 2copab 4642 . 2 class {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})}
131, 12wceq 1475 1 wff USHGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒1-1→(𝒫 𝑣 ∖ {∅})}
 Colors of variables: wff setvar class This definition is referenced by:  relushgra  25824  isushgra  25830
 Copyright terms: Public domain W3C validator