Metamath Proof Explorer


Definition df-ushgr

Description: Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function e is an injective (one-to-one) function into subsets of the set of vertices v , representing the (one or more) vertices incident to the edge. This definition corresponds to the definition of hypergraphs in section I.1 of Bollobas p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of Diestel p. 27, where "E is a subset of [... the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020) (Revised by AV, 8-Oct-2020)

Ref Expression
Assertion df-ushgr USHGraph = g | [˙ Vtx g / v]˙ [˙ iEdg g / e]˙ e : dom e 1-1 𝒫 v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cushgr class USHGraph
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 wf1 wff e : dom e 1-1 𝒫 v
17 16 8 7 wsbc wff [˙ iEdg g / e]˙ e : dom e 1-1 𝒫 v
18 17 5 4 wsbc wff [˙ Vtx g / v]˙ [˙ iEdg g / e]˙ e : dom e 1-1 𝒫 v
19 18 1 cab class g | [˙ Vtx g / v]˙ [˙ iEdg g / e]˙ e : dom e 1-1 𝒫 v
20 0 19 wceq wff USHGraph = g | [˙ Vtx g / v]˙ [˙ iEdg g / e]˙ e : dom e 1-1 𝒫 v