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=iEdgG
Assertion uspgrf1oedg GUSHGraphE:domE1-1 ontoEdgG

Proof

Step Hyp Ref Expression
1 usgrf1o.e E=iEdgG
2 eqid VtxG=VtxG
3 2 1 uspgrf GUSHGraphE:domE1-1x𝒫VtxG|x2
4 f1f1orn E:domE1-1x𝒫VtxG|x2E:domE1-1 ontoranE
5 1 rneqi ranE=raniEdgG
6 edgval EdgG=raniEdgG
7 5 6 eqtr4i ranE=EdgG
8 f1oeq3 ranE=EdgGE:domE1-1 ontoranEE:domE1-1 ontoEdgG
9 7 8 ax-mp E:domE1-1 ontoranEE:domE1-1 ontoEdgG
10 4 9 sylib E:domE1-1x𝒫VtxG|x2E:domE1-1 ontoEdgG
11 3 10 syl GUSHGraphE:domE1-1 ontoEdgG