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 ⊢ E = Edg ⁡ G
uspgredgiedg.i ⊢ I = iEdg ⁡ G
Assertion uspgriedgedg ⊢ G ∈ USHGraph ∧ X ∈ dom ⁡ I → ∃! k ∈ 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 ∈ USHGraph → 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 ∈ USHGraph → 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 ∈ USHGraph → I : dom ⁡ I ⟶ E
9 fdmeu ⊢ I : dom ⁡ I ⟶ E ∧ X ∈ dom ⁡ I → ∃! k ∈ E I ⁡ X = k
10 8 9 sylan ⊢ G ∈ USHGraph ∧ X ∈ dom ⁡ I → ∃! k ∈ E I ⁡ X = k
11 eqcom ⊢ k = I ⁡ X ↔ I ⁡ X = k
12 11 reubii ⊢ ∃! k ∈ E k = I ⁡ X ↔ ∃! k ∈ E I ⁡ X = k
13 10 12 sylibr ⊢ G ∈ USHGraph ∧ X ∈ dom ⁡ I → ∃! k ∈ E k = I ⁡ X