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 ⊢ E = Edg ⁡ G
uspgredgiedg.i ⊢ I = iEdg ⁡ G
Assertion uspgredgiedg ⊢ G ∈ USHGraph ∧ K ∈ E → ∃! x ∈ dom ⁡ I 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 f1oeq3 ⊢ E = Edg ⁡ G → I : dom ⁡ I ⟶ 1-1 onto E ↔ I : dom ⁡ I ⟶ 1-1 onto Edg ⁡ G
5 1 4 ax-mp ⊢ I : dom ⁡ I ⟶ 1-1 onto E ↔ I : dom ⁡ I ⟶ 1-1 onto Edg ⁡ G
6 3 5 sylibr ⊢ G ∈ USHGraph → I : dom ⁡ I ⟶ 1-1 onto E
7 f1ofveu ⊢ I : dom ⁡ I ⟶ 1-1 onto E ∧ K ∈ E → ∃! x ∈ dom ⁡ I I ⁡ x = K
8 6 7 sylan ⊢ G ∈ USHGraph ∧ K ∈ E → ∃! x ∈ dom ⁡ I I ⁡ x = K
9 eqcom ⊢ K = I ⁡ x ↔ I ⁡ x = K
10 9 reubii ⊢ ∃! x ∈ dom ⁡ I K = I ⁡ x ↔ ∃! x ∈ dom ⁡ I I ⁡ x = K
11 8 10 sylibr ⊢ G ∈ USHGraph ∧ K ∈ E → ∃! x ∈ dom ⁡ I K = I ⁡ x