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

Step	Hyp	Ref	Expression
1		cushgr 25723	. 2 class USHGraph
2		ve	. . . . . . . 8 setvar 𝑒
3	2	cv 1474	. . . . . . 7 class 𝑒
4	3	cdm 5038	. . . . . 6 class dom 𝑒
5		vv	. . . . . . . . 9 setvar 𝑣
6	5	cv 1474	. . . . . . . 8 class 𝑣
7	6	cpw 4108	. . . . . . 7 class 𝒫 𝑣
8		c0 3874	. . . . . . . 8 class ∅
9	8	csn 4125	. . . . . . 7 class {∅}
10	7, 9	cdif 3537	. . . . . 6 class (𝒫 𝑣 ∖ {∅})
11	4, 10, 3	wf1 5801	. . . . 5 wff 𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})
12		vg	. . . . . . 7 setvar 𝑔
13	12	cv 1474	. . . . . 6 class 𝑔
14		ciedg 25674	. . . . . 6 class iEdg
15	13, 14	cfv 5804	. . . . 5 class (iEdg‘𝑔)
16	11, 2, 15	wsbc 3402	. . . 4 wff [(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})
17		cvtx 25673	. . . . 5 class Vtx
18	13, 17	cfv 5804	. . . 4 class (Vtx‘𝑔)
19	16, 5, 18	wsbc 3402	. . 3 wff [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})
20	19, 12	cab 2596	. 2 class {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})}
21	1, 20	wceq 1475	1 wff USHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})}

This definition is referenced by:  isushgr  25727