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

Metamath Proof Explorer

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 𝐼 𝐾 = ( 𝐼 ‘ 𝑥 ) )