Theorem uspgredgiedg

Description: In a simple pseudograph, for each edge there is exactly one indexed edge. (Contributed by AV, 20-Apr-2025)

	Ref	Expression
Hypotheses	uspgredgiedg.e	|- E = ( Edg ` G )
	uspgredgiedg.i	|- I = ( iEdg ` G )
Assertion	uspgredgiedg	|- ( ( G e. USPGraph /\ K e. E ) -> E! x e. dom I K = ( I ` x ) )

Proof

Step	Hyp	Ref	Expression
1		uspgredgiedg.e	|- E = ( Edg ` G )
2		uspgredgiedg.i	|- I = ( iEdg ` G )
3	2	uspgrf1oedg	|- ( G e. USPGraph -> I : dom I -1-1-onto-> ( Edg ` G ) )
4		f1oeq3	|- ( E = ( Edg ` G ) -> ( I : dom I -1-1-onto-> E <-> I : dom I -1-1-onto-> ( Edg ` G ) ) )
5	1 4	ax-mp	|- ( I : dom I -1-1-onto-> E <-> I : dom I -1-1-onto-> ( Edg ` G ) )
6	3 5	sylibr	|- ( G e. USPGraph -> I : dom I -1-1-onto-> E )
7		f1ofveu	|- ( ( I : dom I -1-1-onto-> E /\ K e. E ) -> E! x e. dom I ( I ` x ) = K )
8	6 7	sylan	|- ( ( G e. USPGraph /\ K e. E ) -> E! x e. dom I ( I ` x ) = K )
9		eqcom	|- ( K = ( I ` x ) <-> ( I ` x ) = K )
10	9	reubii	|- ( E! x e. dom I K = ( I ` x ) <-> E! x e. dom I ( I ` x ) = K )
11	8 10	sylibr	|- ( ( G e. USPGraph /\ K e. E ) -> E! x e. dom I K = ( I ` x ) )