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 = g | [ ˙ Vtx g / v ] ˙ [ ˙ iEdg g / e ] ˙ e : dom e ⟶ 𝒫 v ∖ ∅
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cuhgr class UHGraph
1
vg setvar g
2
cvtx class Vtx
3
1
cv setvar g
4
3 2
cfv class Vtx g
5
vv setvar v
6
ciedg class iEdg
7
3 6
cfv class iEdg g
8
ve setvar e
9
8
cv setvar e
10
9
cdm class dom e
11
5
cv setvar v
12
11
cpw class 𝒫 v
13
c0 class ∅
14
13
csn class ∅
15
12 14
cdif class 𝒫 v ∖ ∅
16
10 15 9
wf wff e : dom e ⟶ 𝒫 v ∖ ∅
17
16 8 7
wsbc wff [ ˙ iEdg g / e ] ˙ e : dom e ⟶ 𝒫 v ∖ ∅
18
17 5 4
wsbc wff [ ˙ Vtx g / v ] ˙ [ ˙ iEdg g / e ] ˙ e : dom e ⟶ 𝒫 v ∖ ∅
19
18 1
cab class g | [ ˙ Vtx g / v ] ˙ [ ˙ iEdg g / e ] ˙ e : dom e ⟶ 𝒫 v ∖ ∅
20
0 19
wceq wff UHGraph = g | [ ˙ Vtx g / v ] ˙ [ ˙ iEdg g / e ] ˙ e : dom e ⟶ 𝒫 v ∖ ∅