Definition df-umgren 15740

Description: Define the class of all undirected multigraphs. An (undirected) multigraph consists of a set v (of "vertices") and a function e (representing indexed "edges") into subsets of v of cardinality two, representing the two vertices incident to the edge. In contrast to a pseudograph, a multigraph has no loop. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "A multigraph M consists of a finite nonempty set V of vertices and a set E of edges, where every two vertices of M are joined by a finite number of edges (possibly zero). If two or more edges join the same pair of (distinct) vertices, then these edges are called parallel edges." (Contributed by AV, 24-Nov-2020.) (Revised by Jim Kingdon, 3-Jan-2026.)

Assertion

Ref	Expression
df-umgren	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }

Distinct variable group:   e, g, v, x

Detailed syntax breakdown of Definition df-umgren

Step	Hyp	Ref	Expression
1		cumgr 15738	. 2 class UMGraph
2		ve	. . . . . . . 8 setvar e
3	2	cv 1372	. . . . . . 7 class e
4	3	cdm 4680	. . . . . 6 class dom e
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1372	. . . . . . . 8 class x
7		c2o 6506	. . . . . . . 8 class 2o
8		cen 6835	. . . . . . . 8 class ~~
9	6, 7, 8	wbr 4048	. . . . . . 7 wff x ~~ 2o
10		vv	. . . . . . . . 9 setvar v
11	10	cv 1372	. . . . . . . 8 class v
12	11	cpw 3618	. . . . . . 7 class ~P v
13	9, 5, 12	crab 2489	. . . . . 6 class { x e. ~P v | x ~~ 2o }
14	4, 13, 3	wf 5273	. . . . 5 wff e : dom e --> { x e. ~P v | x ~~ 2o }
15		vg	. . . . . . 7 setvar g
16	15	cv 1372	. . . . . 6 class g
17		ciedg 15662	. . . . . 6 class iEdg
18	16, 17	cfv 5277	. . . . 5 class (iEdg ` g )
19	14, 2, 18	wsbc 3000	. . . 4 wff [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o }
20		cvtx 15661	. . . . 5 class Vtx
21	16, 20	cfv 5277	. . . 4 class (Vtx ` g )
22	19, 10, 21	wsbc 3000	. . 3 wff [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o }
23	22, 15	cab 2192	. 2 class { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
24	1, 23	wceq 1373	1 wff UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }

This definition is referenced by:  isumgren  15751