Definition df-uhgrm 15709

Description: Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into the set of inhabited subsets of this set. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by Jim Kingdon, 29-Dec-2025.)

Assertion

Ref	Expression
df-uhgrm	⊢ UHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}}

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

Detailed syntax breakdown of Definition df-uhgrm

Step	Hyp	Ref	Expression
1		cuhgr 15707	. 2 class UHGraph
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	wf 5272	. . . . 5 wff 𝑒:dom 𝑒⟶{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}
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 𝑒⟶{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}
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 𝑒⟶{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}
22	21, 14	cab 2192	. 2 class {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}}
23	1, 22	wceq 1373	1 wff UHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}}

This definition is referenced by:  isuhgrm  15711