This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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