Definition df-umgren 15740

Description: Define the class of all undirected multigraphs. An (undirected) multigraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into subsets of 𝑣 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 = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ 𝒫 𝑣 ∣ 𝑥 ≈ 2o}}

Distinct variable group:   𝑒,𝑔,𝑣,𝑥

Detailed syntax breakdown of Definition df-umgren

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

This definition is referenced by:  isumgren  15751