Definition df-uspgr

Description: Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr ) or a special undirected simple hypergraph (see uspgrushgr ), consisting of a set v (of "vertices") and an injective (one-to-one) function e (representing (indexed) "edges") into subsets of v of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a pseudograph, there is at most one edge between two vertices resp. at most one loop for a vertex. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 13-Oct-2020)

	Ref	Expression
Assertion	df-uspgr	$$⊢\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}{⟶}\left\{x\in \left(𝒫v\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuspgr	$$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		vx	$$setvarx$$
12	5	cv	$$setvarv$$
13	12	cpw	$$class𝒫v$$
14		c0	$$class\varnothing$$
15	14	csn	$$class\left\{\varnothing \right\}$$
16	13 15	cdif	$$class\left(𝒫v\setminus \left\{\varnothing \right\}\right)$$
17		chash	$$class\left|.\right|$$
18	11	cv	$$setvarx$$
19	18 17	cfv	$$class\left|x\right|$$
20		cle	$$class\le$$
21		c2	$$class2$$
22	19 21 20	wbr	$$wff\left|x\right|\le 2$$
23	22 11 16	crab	$$class\left\{x\in \left(𝒫v\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
24	10 23 9	wf1	$$wffe:\mathrm{dom}e\underset{1-1}{⟶}\left\{x\in \left(𝒫v\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
25	24 8 7	wsbc	$$wff\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}e:\mathrm{dom}e\underset{1-1}{⟶}\left\{x\in \left(𝒫v\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
26	25 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}{⟶}\left\{x\in \left(𝒫v\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
27	26 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}{⟶}\left\{x\in \left(𝒫v\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\right\}$$
28	0 27	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}{⟶}\left\{x\in \left(𝒫v\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\right\}$$