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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvex | |
|
2 | 1 | dmex | |
3 | eqid | |
|
4 | eqid | |
|
5 | 3 4 | usgrf | |
6 | hashf1rn | |
|
7 | 2 5 6 | sylancr | |
8 | edgval | |
|
9 | 8 | a1i | |
10 | 9 | fveq2d | |
11 | 7 10 | eqtr4d | |