Definition df-ushgr 29667

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

Step	Hyp	Ref	Expression
1		cushgr 29665	. 2 class USHGraph
2		ve	. . . . . . . 8 setvar 𝑒
3	2	cv 1569	. . . . . . 7 class 𝑒
4	3	cdm 5655	. . . . . 6 class dom 𝑒
5		vv	. . . . . . . . 9 setvar 𝑣
6	5	cv 1569	. . . . . . . 8 class 𝑣
7	6	cpw 4560	. . . . . . 7 class 𝒫 𝑣
8		c0 4281	. . . . . . . 8 class ∅
9	8	csn 4588	. . . . . . 7 class {∅}
10	7, 9	cdif 4048	. . . . . 6 class (𝒫 𝑣 ∖ {∅})
11	4, 10, 3	wf1 6555	. . . . 5 wff 𝑒:dom 𝑒⟶1-1(𝒫 𝑣 ∖ {∅})
12		vg	. . . . . . 7 setvar 𝑔
13	12	cv 1569	. . . . . 6 class 𝑔
14		ciedg 29605	. . . . . 6 class iEdg
15	13, 14	cfv 6558	. . . . 5 class (iEdg‘𝑔)
16	11, 2, 15	wsbc 3742	. . . 4 wff [(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶1-1(𝒫 𝑣 ∖ {∅})
17		cvtx 29604	. . . . 5 class Vtx
18	13, 17	cfv 6558	. . . 4 class (Vtx‘𝑔)
19	16, 5, 18	wsbc 3742	. . 3 wff [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶1-1(𝒫 𝑣 ∖ {∅})
20	19, 12	cab 2741	. 2 class {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶1-1(𝒫 𝑣 ∖ {∅})}
21	1, 20	wceq 1570	1 wff USHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶1-1(𝒫 𝑣 ∖ {∅})}

This definition is used by:  isushgr  29669