![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-ushgr | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-ushgr | ⊢ USHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cushgr 28297 | . 2 class USHGraph | |
2 | ve | . . . . . . . 8 setvar 𝑒 | |
3 | 2 | cv 1541 | . . . . . . 7 class 𝑒 |
4 | 3 | cdm 5675 | . . . . . 6 class dom 𝑒 |
5 | vv | . . . . . . . . 9 setvar 𝑣 | |
6 | 5 | cv 1541 | . . . . . . . 8 class 𝑣 |
7 | 6 | cpw 4601 | . . . . . . 7 class 𝒫 𝑣 |
8 | c0 4321 | . . . . . . . 8 class ∅ | |
9 | 8 | csn 4627 | . . . . . . 7 class {∅} |
10 | 7, 9 | cdif 3944 | . . . . . 6 class (𝒫 𝑣 ∖ {∅}) |
11 | 4, 10, 3 | wf1 6537 | . . . . 5 wff 𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅}) |
12 | vg | . . . . . . 7 setvar 𝑔 | |
13 | 12 | cv 1541 | . . . . . 6 class 𝑔 |
14 | ciedg 28237 | . . . . . 6 class iEdg | |
15 | 13, 14 | cfv 6540 | . . . . 5 class (iEdg‘𝑔) |
16 | 11, 2, 15 | wsbc 3776 | . . . 4 wff [(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅}) |
17 | cvtx 28236 | . . . . 5 class Vtx | |
18 | 13, 17 | cfv 6540 | . . . 4 class (Vtx‘𝑔) |
19 | 16, 5, 18 | wsbc 3776 | . . 3 wff [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅}) |
20 | 19, 12 | cab 2710 | . 2 class {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})} |
21 | 1, 20 | wceq 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 |