Theorem uspgrf1oedg

Description: The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020) (Revised by AV, 15-Oct-2020)

	Ref	Expression
Hypothesis	usgrf1o.e	|- E = ( iEdg ` G )
Assertion	uspgrf1oedg	|- ( G e. USPGraph -> E : dom E -1-1-onto-> ( Edg ` G ) )

Proof

Step	Hyp	Ref	Expression
1		usgrf1o.e	|- E = ( iEdg ` G )
2		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
3	2 1	uspgrf	|- ( G e. USPGraph -> E : dom E -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
4		f1f1orn	|- ( E : dom E -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> E : dom E -1-1-onto-> ran E )
5	1	rneqi	|- ran E = ran ( iEdg ` G )
6		edgval	|- ( Edg ` G ) = ran ( iEdg ` G )
7	5 6	eqtr4i	|- ran E = ( Edg ` G )
8		f1oeq3	|- ( ran E = ( Edg ` G ) -> ( E : dom E -1-1-onto-> ran E <-> E : dom E -1-1-onto-> ( Edg ` G ) ) )
9	7 8	ax-mp	|- ( E : dom E -1-1-onto-> ran E <-> E : dom E -1-1-onto-> ( Edg ` G ) )
10	4 9	sylib	|- ( E : dom E -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> E : dom E -1-1-onto-> ( Edg ` G ) )
11	3 10	syl	|- ( G e. USPGraph -> E : dom E -1-1-onto-> ( Edg ` G ) )