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