Definition df-uspgr

Description: Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr ) or a special undirected simple hypergraph (see uspgrushgr ), consisting of a set v (of "vertices") and an injective (one-to-one) 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. In contrast to a pseudograph, there is at most one edge between two vertices resp. at most one loop for a vertex. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 13-Oct-2020)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuspgr	⊢ USPGraph
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	wf1	⊢ 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
25	24 8 7	wsbc	⊢ [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
26	25 5 4	wsbc	⊢ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
27	26 1	cab	⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } }
28	0 27	wceq	⊢ USPGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } }