Metamath Proof Explorer


Theorem usgrsizedg

Description: In a simple graph, the size of the edge function is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020) (Revised by AV, 7-Jun-2021)

Ref Expression
Assertion usgrsizedg GUSGraphiEdgG=EdgG

Proof

Step Hyp Ref Expression
1 fvex iEdgGV
2 1 dmex domiEdgGV
3 eqid VtxG=VtxG
4 eqid iEdgG=iEdgG
5 3 4 usgrf GUSGraphiEdgG:domiEdgG1-1x𝒫VtxG|x=2
6 hashf1rn domiEdgGViEdgG:domiEdgG1-1x𝒫VtxG|x=2iEdgG=raniEdgG
7 2 5 6 sylancr GUSGraphiEdgG=raniEdgG
8 edgval EdgG=raniEdgG
9 8 a1i GUSGraphEdgG=raniEdgG
10 9 fveq2d GUSGraphEdgG=raniEdgG
11 7 10 eqtr4d GUSGraphiEdgG=EdgG