This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Undirected hypergraphs 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 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) }