Definition df-uslgra 25059

Description: Define the class of all undirected simple graphs with loops. An undirected simple graph with loops is a special undirected multigraph <. V , E >. where E is an injective (one-to-one) function 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 multigraph, there is at most one edge between two vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

Assertion

Ref	Expression
df-uslgra	|- USLGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }

Distinct variable group:   v, e, x

Detailed syntax breakdown of Definition df-uslgra

Step	Hyp	Ref	Expression
1		cuslg 25056	. 2 class USLGrph
2		ve	. . . . . 6 setvar e
3	2	cv 1443	. . . . 5 class e
4	3	cdm 4834	. . . 4 class dom e
5		vx	. . . . . . . 8 setvar x
6	5	cv 1443	. . . . . . 7 class x
7		chash 12515	. . . . . . 7 class #
8	6, 7	cfv 5582	. . . . . 6 class ( # ` x )
9		c2 10659	. . . . . 6 class 2
10		cle 9676	. . . . . 6 class <_
11	8, 9, 10	wbr 4402	. . . . 5 wff ( # ` x ) <_ 2
12		vv	. . . . . . . 8 setvar v
13	12	cv 1443	. . . . . . 7 class v
14	13	cpw 3951	. . . . . 6 class ~P v
15		c0 3731	. . . . . . 7 class (/)
16	15	csn 3968	. . . . . 6 class { (/) }
17	14, 16	cdif 3401	. . . . 5 class ( ~P v \ { (/) } )
18	11, 5, 17	crab 2741	. . . 4 class { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
19	4, 18, 3	wf1 5579	. . 3 wff e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 }
20	19, 12, 2	copab 4460	. 2 class { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }
21	1, 20	wceq 1444	1 wff USLGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }

This definition is referenced by:  reluslgra  25061  isuslgra  25070