This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐼 ) → ∃! 𝑘 ∈ 𝐸 𝑘 = ( 𝐼 ‘ 𝑋 ) )