Definition df-uhgr 25953

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 power set of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 8-Oct-2020.)

Assertion

Ref	Expression
df-uhgr	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } ) }

Distinct variable group:   e, g, v

Detailed syntax breakdown of Definition df-uhgr

Step	Hyp	Ref	Expression
1		cuhgr 25951	. 2 class UHGraph
2		ve	. . . . . . . 8 setvar e
3	2	cv 1482	. . . . . . 7 class e
4	3	cdm 5114	. . . . . 6 class dom e
5		vv	. . . . . . . . 9 setvar v
6	5	cv 1482	. . . . . . . 8 class v
7	6	cpw 4158	. . . . . . 7 class ~P v
8		c0 3915	. . . . . . . 8 class (/)
9	8	csn 4177	. . . . . . 7 class { (/) }
10	7, 9	cdif 3571	. . . . . 6 class ( ~P v \ { (/) } )
11	4, 10, 3	wf 5884	. . . . 5 wff e : dom e --> ( ~P v \ { (/) } )
12		vg	. . . . . . 7 setvar g
13	12	cv 1482	. . . . . 6 class g
14		ciedg 25875	. . . . . 6 class iEdg
15	13, 14	cfv 5888	. . . . 5 class (iEdg ` g )
16	11, 2, 15	wsbc 3435	. . . 4 wff [. (iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } )
17		cvtx 25874	. . . . 5 class Vtx
18	13, 17	cfv 5888	. . . 4 class (Vtx ` g )
19	16, 5, 18	wsbc 3435	. . 3 wff [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } )
20	19, 12	cab 2608	. 2 class { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } ) }
21	1, 20	wceq 1483	1 wff UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } ) }

This definition is referenced by:  isuhgr  25955