Metamath Proof Explorer


Definition df-usgr

Description: Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr ), consisting of a set v (of "vertices") and an injective (one-to-one) function e (representing (indexed) "edges") into subsets of v 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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cusgr USGraph
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 c2 2
21 19 20 wceq ( ♯ ‘ 𝑥 ) = 2
22 21 11 16 crab { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
23 10 22 9 wf1 𝑒 : dom 𝑒1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
24 23 8 7 wsbc [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
25 24 5 4 wsbc [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
26 25 1 cab { 𝑔[ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } }
27 0 26 wceq USGraph = { 𝑔[ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒1-1→ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } }