Definition df-usgr 27502

Description: Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr 27529), consisting of a set 𝑣 (of "vertices") and an injective (one-to-one) function 𝑒 (representing (indexed) "edges") into subsets of 𝑣 of cardinality two, representing the two vertices incident to the edge. In contrast to an undirected simple pseudograph, an undirected simple graph has no loops (edges connecting a vertex with itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.)

Assertion

Ref	Expression
df-usgr	⊢ USGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}}

Distinct variable group:   𝑒,𝑔,𝑣,𝑥

Detailed syntax breakdown of Definition df-usgr

Step	Hyp	Ref	Expression
1		cusgr 27500	. 2 class USGraph
2		ve	. . . . . . . 8 setvar 𝑒
3	2	cv 1540	. . . . . . 7 class 𝑒
4	3	cdm 5588	. . . . . 6 class dom 𝑒
5		vx	. . . . . . . . . 10 setvar 𝑥
6	5	cv 1540	. . . . . . . . 9 class 𝑥
7		chash 14025	. . . . . . . . 9 class ♯
8	6, 7	cfv 6430	. . . . . . . 8 class (♯‘𝑥)
9		c2 12011	. . . . . . . 8 class 2
10	8, 9	wceq 1541	. . . . . . 7 wff (♯‘𝑥) = 2
11		vv	. . . . . . . . . 10 setvar 𝑣
12	11	cv 1540	. . . . . . . . 9 class 𝑣
13	12	cpw 4538	. . . . . . . 8 class 𝒫 𝑣
14		c0 4261	. . . . . . . . 9 class ∅
15	14	csn 4566	. . . . . . . 8 class {∅}
16	13, 15	cdif 3888	. . . . . . 7 class (𝒫 𝑣 ∖ {∅})
17	10, 5, 16	crab 3069	. . . . . 6 class {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}
18	4, 17, 3	wf1 6427	. . . . 5 wff 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}
19		vg	. . . . . . 7 setvar 𝑔
20	19	cv 1540	. . . . . 6 class 𝑔
21		ciedg 27348	. . . . . 6 class iEdg
22	20, 21	cfv 6430	. . . . 5 class (iEdg‘𝑔)
23	18, 2, 22	wsbc 3719	. . . 4 wff [(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}
24		cvtx 27347	. . . . 5 class Vtx
25	20, 24	cfv 6430	. . . 4 class (Vtx‘𝑔)
26	23, 11, 25	wsbc 3719	. . 3 wff [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}
27	26, 19	cab 2716	. 2 class {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}}
28	1, 27	wceq 1541	1 wff USGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}}

This definition is referenced by:  isusgr  27504