Metamath Proof Explorer


Definition df-upgr

Description: Define the class of all undirected pseudographs. An (undirected) pseudograph consists of a set v (of "vertices") and a 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. 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: "In a pseudograph, not only are parallel edges permitted but an edge is also permitted to join a vertex to itself. Such an edge is called a loop." (in contrast to a multigraph, see df-umgr ). (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 24-Nov-2020)

Ref Expression
Assertion df-upgr UPGraph = g | [˙ Vtx g / v]˙ [˙ iEdg g / e]˙ e : dom e x 𝒫 v | x 2

Detailed syntax breakdown

Step Hyp Ref Expression
0 cupgr class UPGraph
1 vg setvar g
2 cvtx class Vtx
3 1 cv setvar g
4 3 2 cfv class Vtx g
5 vv setvar v
6 ciedg class iEdg
7 3 6 cfv class iEdg g
8 ve setvar e
9 8 cv setvar e
10 9 cdm class dom e
11 vx setvar x
12 5 cv setvar v
13 12 cpw class 𝒫 v
14 c0 class
15 14 csn class
16 13 15 cdif class 𝒫 v
17 chash class .
18 11 cv setvar x
19 18 17 cfv class x
20 cle class
21 c2 class 2
22 19 21 20 wbr wff x 2
23 22 11 16 crab class x 𝒫 v | x 2
24 10 23 9 wf wff e : dom e x 𝒫 v | x 2
25 24 8 7 wsbc wff [˙ iEdg g / e]˙ e : dom e x 𝒫 v | x 2
26 25 5 4 wsbc wff [˙ Vtx g / v]˙ [˙ iEdg g / e]˙ e : dom e x 𝒫 v | x 2
27 26 1 cab class g | [˙ Vtx g / v]˙ [˙ iEdg g / e]˙ e : dom e x 𝒫 v | x 2
28 0 27 wceq wff UPGraph = g | [˙ Vtx g / v]˙ [˙ iEdg g / e]˙ e : dom e x 𝒫 v | x 2