Theorem usgrf1oedg

Description: The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020)

	Ref	Expression
Hypotheses	usgrf1oedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	usgrf1oedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	usgrf1oedg	⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		usgrf1oedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2		usgrf1oedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4	3 1	usgrf	⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5		f1f1orn	⊢ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
6	4 5	syl	⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
7		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
8	7	a1i	⊢ ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
9	1	eqcomi	⊢ ( iEdg ‘ 𝐺 ) = 𝐼
10	9	rneqi	⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼
11	8 10	eqtrdi	⊢ ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) = ran 𝐼 )
12	2 11	syl5eq	⊢ ( 𝐺 ∈ USGraph → 𝐸 = ran 𝐼 )
13	12	f1oeq3d	⊢ ( 𝐺 ∈ USGraph → ( 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 ↔ 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ) )
14	6 13	mpbird	⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 )