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