This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 ) ) )