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 = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cupgr ⊢ UPGraph
1 vg ⊢ 𝑔
2 cvtx ⊢ Vtx
3 1 cv ⊢ 𝑔
4 3 2 cfv ⊢ ( Vtx ‘ 𝑔 )
5 vv ⊢ 𝑣
6 ciedg ⊢ iEdg
7 3 6 cfv ⊢ ( iEdg ‘ 𝑔 )
8 ve ⊢ 𝑒
9 8 cv ⊢ 𝑒
10 9 cdm ⊢ dom 𝑒
11 vx ⊢ 𝑥
12 5 cv ⊢ 𝑣
13 12 cpw ⊢ 𝒫 𝑣
14 c0 ⊢ ∅
15 14 csn ⊢ { ∅ }
16 13 15 cdif ⊢ ( 𝒫 𝑣 ∖ { ∅ } )
17 chash ⊢ ♯
18 11 cv ⊢ 𝑥
19 18 17 cfv ⊢ ( ♯ ‘ 𝑥 )
20 cle ⊢ ≤
21 c2 ⊢ 2
22 19 21 20 wbr ⊢ ( ♯ ‘ 𝑥 ) ≤ 2
23 22 11 16 crab ⊢ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
24 10 23 9 wf ⊢ 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
25 24 8 7 wsbc ⊢ [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
26 25 5 4 wsbc ⊢ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
27 26 1 cab ⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } }
28 0 27 wceq ⊢ UPGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } }