Definition df-ushgrm 15710

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 Jim Kingdon, 31-Dec-2025.)

Assertion

Ref	Expression
df-ushgrm	⊢ USHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}}

Distinct variable group:   𝑒,𝑔,𝑗,𝑠,𝑣

Detailed syntax breakdown of Definition df-ushgrm

Step	Hyp	Ref	Expression
1		cushgr 15708	. 2 class USHGraph
2		ve	. . . . . . . 8 setvar 𝑒
3	2	cv 1372	. . . . . . 7 class 𝑒
4	3	cdm 4679	. . . . . 6 class dom 𝑒
5		vj	. . . . . . . . 9 setvar 𝑗
6		vs	. . . . . . . . 9 setvar 𝑠
7	5, 6	wel 2178	. . . . . . . 8 wff 𝑗 ∈ 𝑠
8	7, 5	wex 1516	. . . . . . 7 wff ∃𝑗 𝑗 ∈ 𝑠
9		vv	. . . . . . . . 9 setvar 𝑣
10	9	cv 1372	. . . . . . . 8 class 𝑣
11	10	cpw 3617	. . . . . . 7 class 𝒫 𝑣
12	8, 6, 11	crab 2489	. . . . . 6 class {𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}
13	4, 12, 3	wf1 5273	. . . . 5 wff 𝑒:dom 𝑒–1-1→{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}
14		vg	. . . . . . 7 setvar 𝑔
15	14	cv 1372	. . . . . 6 class 𝑔
16		ciedg 15656	. . . . . 6 class iEdg
17	15, 16	cfv 5276	. . . . 5 class (iEdg‘𝑔)
18	13, 2, 17	wsbc 2999	. . . 4 wff [(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}
19		cvtx 15655	. . . . 5 class Vtx
20	15, 19	cfv 5276	. . . 4 class (Vtx‘𝑔)
21	18, 9, 20	wsbc 2999	. . 3 wff [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}
22	21, 14	cab 2192	. 2 class {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}}
23	1, 22	wceq 1373	1 wff USHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}}

This definition is referenced by:  isushgrm  15712