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 ⊢ G ∈ USGraph → iEdg ⁡ G = Edg ⁡ G

Proof

Step Hyp Ref Expression
1 fvex ⊢ iEdg ⁡ G ∈ V
2 1 dmex ⊢ dom ⁡ iEdg ⁡ G ∈ V
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 3 4 usgrf ⊢ G ∈ USGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
6 hashf1rn ⊢ dom ⁡ iEdg ⁡ G ∈ V ∧ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2 → iEdg ⁡ G = ran ⁡ iEdg ⁡ G
7 2 5 6 sylancr ⊢ G ∈ USGraph → iEdg ⁡ G = ran ⁡ iEdg ⁡ G
8 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
9 8 a1i ⊢ G ∈ USGraph → Edg ⁡ G = ran ⁡ iEdg ⁡ G
10 9 fveq2d ⊢ G ∈ USGraph → Edg ⁡ G = ran ⁡ iEdg ⁡ G
11 7 10 eqtr4d ⊢ G ∈ USGraph → iEdg ⁡ G = Edg ⁡ G