Theorem usgrfun

Description: The edge function of a simple graph is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017) (Revised by AV, 13-Oct-2020)

	Ref	Expression
Assertion	usgrfun	⊢ ( 𝐺 ∈ USGraph → Fun ( iEdg ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3	1 2	usgrfs	⊢ ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
4		f1fun	⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → Fun ( iEdg ‘ 𝐺 ) )
5	3 4	syl	⊢ ( 𝐺 ∈ USGraph → Fun ( iEdg ‘ 𝐺 ) )