Metamath Proof Explorer


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 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) }