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	$$⊢\mathrm{USHGraph}=\left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cushgr	$$class\mathrm{USHGraph}$$
1		vg	$$setvarg$$
2		cvtx	$$class\mathrm{Vtx}$$
3	1	cv	$$setvarg$$
4	3 2	cfv	$$class\mathrm{Vtx}\left(g\right)$$
5		vv	$$setvarv$$
6		ciedg	$$class\mathrm{iEdg}$$
7	3 6	cfv	$$class\mathrm{iEdg}\left(g\right)$$
8		ve	$$setvare$$
9	8	cv	$$setvare$$
10	9	cdm	$$class\mathrm{dom}e$$
11	5	cv	$$setvarv$$
12	11	cpw	$$class𝒫v$$
13		c0	$$class\varnothing$$
14	13	csn	$$class\left\{\varnothing \right\}$$
15	12 14	cdif	$$class\left(𝒫v\setminus \left\{\varnothing \right\}\right)$$
16	10 15 9	wf1	$$wffe:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}$$
17	16 8 7	wsbc	$$wff\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}$$
18	17 5 4	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}$$
19	18 1	cab	$$class\left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\right\}$$
20	0 19	wceq	$$wff\mathrm{USHGraph}=\left\{g|\underset{\dot{}}{[}\mathrm{Vtx}\left(g\right)/v\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}𝒫v\setminus \left\{\varnothing \right\}\right\}$$