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	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	uspgredgiedg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	uspgriedgedg	⊢ ( ( 𝐺 ∈ 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		f1of	⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) → 𝐼 : dom 𝐼 ⟶ ( Edg ‘ 𝐺 ) )
5	3 4	syl	⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 ⟶ ( Edg ‘ 𝐺 ) )
6		feq3	⊢ ( 𝐸 = ( Edg ‘ 𝐺 ) → ( 𝐼 : dom 𝐼 ⟶ 𝐸 ↔ 𝐼 : dom 𝐼 ⟶ ( Edg ‘ 𝐺 ) ) )
7	1 6	ax-mp	⊢ ( 𝐼 : dom 𝐼 ⟶ 𝐸 ↔ 𝐼 : dom 𝐼 ⟶ ( Edg ‘ 𝐺 ) )
8	5 7	sylibr	⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 ⟶ 𝐸 )
9		fdmeu	⊢ ( ( 𝐼 : dom 𝐼 ⟶ 𝐸 ∧ 𝑋 ∈ dom 𝐼 ) → ∃! 𝑘 ∈ 𝐸 ( 𝐼 ‘ 𝑋 ) = 𝑘 )
10	8 9	sylan	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ dom 𝐼 ) → ∃! 𝑘 ∈ 𝐸 ( 𝐼 ‘ 𝑋 ) = 𝑘 )
11		eqcom	⊢ ( 𝑘 = ( 𝐼 ‘ 𝑋 ) ↔ ( 𝐼 ‘ 𝑋 ) = 𝑘 )
12	11	reubii	⊢ ( ∃! 𝑘 ∈ 𝐸 𝑘 = ( 𝐼 ‘ 𝑋 ) ↔ ∃! 𝑘 ∈ 𝐸 ( 𝐼 ‘ 𝑋 ) = 𝑘 )
13	10 12	sylibr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑋 ∈ dom 𝐼 ) → ∃! 𝑘 ∈ 𝐸 𝑘 = ( 𝐼 ‘ 𝑋 ) )