Definition df-uhgr

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuhgr	|- UHGraph
1		vg	|- g
2		cvtx	|- Vtx
3	1	cv	|- g
4	3 2	cfv	|- ( Vtx ` g )
5		vv	|- v
6		ciedg	|- iEdg
7	3 6	cfv	|- ( iEdg ` g )
8		ve	|- e
9	8	cv	|- e
10	9	cdm	|- dom e
11	5	cv	|- v
12	11	cpw	|- ~P v
13		c0	|- (/)
14	13	csn	|- { (/) }
15	12 14	cdif	|- ( ~P v \ { (/) } )
16	10 15 9	wf	|- e : dom e --> ( ~P v \ { (/) } )
17	16 8 7	wsbc	|- [. ( iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } )
18	17 5 4	wsbc	|- [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } )
19	18 1	cab	|- { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } ) }
20	0 19	wceq	|- UHGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> ( ~P v \ { (/) } ) }