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	|- USPGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuspgr	|- USPGraph
1		vg	|- g
2		cvtx	|- Vtx
3	1	cv	|- g
4	3 2	cfv	|- ( Vtx ` g )
5		vv	|- v
6		ciedg	|- iEdg
7	3 6	cfv	|- ( iEdg ` g )
8		ve	|- e
9	8	cv	|- e
10	9	cdm	|- dom e
11		vx	|- x
12	5	cv	|- v
13	12	cpw	|- ~P v
14		c0	|- (/)
15	14	csn	|- { (/) }
16	13 15	cdif	|- ( ~P v \ { (/) } )
17		chash	|- #
18	11	cv	|- x
19	18 17	cfv	|- ( # ` x )
20		cle	|- <_
21		c2	|- 2
22	19 21 20	wbr	|- ( # ` x ) <_ 2
23	22 11 16	crab	|- { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
24	10 23 9	wf1	|- e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
25	24 8 7	wsbc	|- [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
26	25 5 4	wsbc	|- [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
27	26 1	cab	|- { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }
28	0 27	wceq	|- USPGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }