Theorem uspgriedgedg

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

	Ref	Expression
Hypotheses	uspgredgiedg.e	|- E = ( Edg ` G )
	uspgredgiedg.i	|- I = ( iEdg ` G )
Assertion	uspgriedgedg	|- ( ( G e. USPGraph /\ X e. dom I ) -> E! k e. E 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		f1of	|- ( I : dom I -1-1-onto-> ( Edg ` G ) -> I : dom I --> ( Edg ` G ) )
5	3 4	syl	|- ( G e. USPGraph -> I : dom I --> ( Edg ` G ) )
6		feq3	|- ( E = ( Edg ` G ) -> ( I : dom I --> E <-> I : dom I --> ( Edg ` G ) ) )
7	1 6	ax-mp	|- ( I : dom I --> E <-> I : dom I --> ( Edg ` G ) )
8	5 7	sylibr	|- ( G e. USPGraph -> I : dom I --> E )
9		fdmeu	|- ( ( I : dom I --> E /\ X e. dom I ) -> E! k e. E ( I ` X ) = k )
10	8 9	sylan	|- ( ( G e. USPGraph /\ X e. dom I ) -> E! k e. E ( I ` X ) = k )
11		eqcom	|- ( k = ( I ` X ) <-> ( I ` X ) = k )
12	11	reubii	|- ( E! k e. E k = ( I ` X ) <-> E! k e. E ( I ` X ) = k )
13	10 12	sylibr	|- ( ( G e. USPGraph /\ X e. dom I ) -> E! k e. E k = ( I ` X ) )