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 ( 𝐺 ∈ USGraph → ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) = ( ♯ ‘ ( Edg ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 fvex ( iEdg ‘ 𝐺 ) ∈ V
2 1 dmex dom ( iEdg ‘ 𝐺 ) ∈ V
3 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5 3 4 usgrf ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
6 hashf1rn ( ( dom ( iEdg ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) → ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) = ( ♯ ‘ ran ( iEdg ‘ 𝐺 ) ) )
7 2 5 6 sylancr ( 𝐺 ∈ USGraph → ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) = ( ♯ ‘ ran ( iEdg ‘ 𝐺 ) ) )
8 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
9 8 a1i ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
10 9 fveq2d ( 𝐺 ∈ USGraph → ( ♯ ‘ ( Edg ‘ 𝐺 ) ) = ( ♯ ‘ ran ( iEdg ‘ 𝐺 ) ) )
11 7 10 eqtr4d ( 𝐺 ∈ USGraph → ( ♯ ‘ ( iEdg ‘ 𝐺 ) ) = ( ♯ ‘ ( Edg ‘ 𝐺 ) ) )