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	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	uspgredgiedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	uspgredgiedg	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐾 ∈ 𝐸 ) → ∃! 𝑥 ∈ dom 𝐼 𝐾 = ( 𝐼 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		uspgredgiedg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2		uspgredgiedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3	2	uspgrf1oedg	⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) )
4		f1oeq3	⊢ ( 𝐸 = ( Edg ‘ 𝐺 ) → ( 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 ↔ 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) ) )
5	1 4	ax-mp	⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 ↔ 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) )
6	3 5	sylibr	⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 )
7		f1ofveu	⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ 𝐸 ∧ 𝐾 ∈ 𝐸 ) → ∃! 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = 𝐾 )
8	6 7	sylan	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐾 ∈ 𝐸 ) → ∃! 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = 𝐾 )
9		eqcom	⊢ ( 𝐾 = ( 𝐼 ‘ 𝑥 ) ↔ ( 𝐼 ‘ 𝑥 ) = 𝐾 )
10	9	reubii	⊢ ( ∃! 𝑥 ∈ dom 𝐼 𝐾 = ( 𝐼 ‘ 𝑥 ) ↔ ∃! 𝑥 ∈ dom 𝐼 ( 𝐼 ‘ 𝑥 ) = 𝐾 )
11	8 10	sylibr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐾 ∈ 𝐸 ) → ∃! 𝑥 ∈ dom 𝐼 𝐾 = ( 𝐼 ‘ 𝑥 ) )