Definition df-uhgrm 16056

Description: Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set v (of "vertices") and a function e (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 = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }

Distinct variable group:   e, g, j, s, v

Detailed syntax breakdown of Definition df-uhgrm

Step	Hyp	Ref	Expression
1		cuhgr 16054	. 2 class UHGraph
2		ve	. . . . . . . 8 setvar e
3	2	cv 1397	. . . . . . 7 class e
4	3	cdm 4748	. . . . . 6 class dom e
5		vj	. . . . . . . . 9 setvar j
6		vs	. . . . . . . . 9 setvar s
7	5, 6	wel 2204	. . . . . . . 8 wff j e. s
8	7, 5	wex 1541	. . . . . . 7 wff E. j j e. s
9		vv	. . . . . . . . 9 setvar v
10	9	cv 1397	. . . . . . . 8 class v
11	10	cpw 3668	. . . . . . 7 class ~P v
12	8, 6, 11	crab 2524	. . . . . 6 class { s e. ~P v | E. j j e. s }
13	4, 12, 3	wf 5347	. . . . 5 wff e : dom e --> { s e. ~P v | E. j j e. s }
14		vg	. . . . . . 7 setvar g
15	14	cv 1397	. . . . . 6 class g
16		ciedg 16000	. . . . . 6 class iEdg
17	15, 16	cfv 5351	. . . . 5 class (iEdg ` g )
18	13, 2, 17	wsbc 3041	. . . 4 wff [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s }
19		cvtx 15999	. . . . 5 class Vtx
20	15, 19	cfv 5351	. . . 4 class (Vtx ` g )
21	18, 9, 20	wsbc 3041	. . 3 wff [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s }
22	21, 14	cab 2218	. 2 class { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
23	1, 22	wceq 1398	1 wff UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }

This definition is referenced by:  isuhgrm  16058