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 = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuhgr	⊢ UHGraph
1		vg	⊢ 𝑔
2		cvtx	⊢ Vtx
3	1	cv	⊢ 𝑔
4	3 2	cfv	⊢ ( Vtx ‘ 𝑔 )
5		vv	⊢ 𝑣
6		ciedg	⊢ iEdg
7	3 6	cfv	⊢ ( iEdg ‘ 𝑔 )
8		ve	⊢ 𝑒
9	8	cv	⊢ 𝑒
10	9	cdm	⊢ dom 𝑒
11	5	cv	⊢ 𝑣
12	11	cpw	⊢ 𝒫 𝑣
13		c0	⊢ ∅
14	13	csn	⊢ { ∅ }
15	12 14	cdif	⊢ ( 𝒫 𝑣 ∖ { ∅ } )
16	10 15 9	wf	⊢ 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } )
17	16 8 7	wsbc	⊢ [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } )
18	17 5 4	wsbc	⊢ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } )
19	18 1	cab	⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) }
20	0 19	wceq	⊢ UHGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) }