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

Metamath Proof Explorer

Theorem uspgrf1oedg

Description: The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020) (Revised by AV, 15-Oct-2020)

Ref Expression
Hypothesis usgrf1o.e ⊢ E = iEdg ⁡ G
Assertion uspgrf1oedg ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G

Proof

Step Hyp Ref Expression
1 usgrf1o.e ⊢ E = iEdg ⁡ G
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 2 1 uspgrf ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
4 f1f1orn ⊢ E : dom ⁡ E ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E
5 1 rneqi ⊢ ran ⁡ E = ran ⁡ iEdg ⁡ G
6 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
7 5 6 eqtr4i ⊢ ran ⁡ E = Edg ⁡ G
8 f1oeq3 ⊢ ran ⁡ E = Edg ⁡ G → E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ↔ E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G
9 7 8 ax-mp ⊢ E : dom ⁡ E ⟶ 1-1 onto ran ⁡ E ↔ E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G
10 4 9 sylib ⊢ E : dom ⁡ E ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 → E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G
11 3 10 syl ⊢ G ∈ USHGraph → E : dom ⁡ E ⟶ 1-1 onto Edg ⁡ G