Metamath Proof Explorer


Theorem usgrf1oedg

Description: The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020)

Ref Expression
Hypotheses usgrf1oedg.i I=iEdgG
usgrf1oedg.e E=EdgG
Assertion usgrf1oedg GUSGraphI:domI1-1 ontoE

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i I=iEdgG
2 usgrf1oedg.e E=EdgG
3 eqid VtxG=VtxG
4 3 1 usgrf GUSGraphI:domI1-1x𝒫VtxG|x=2
5 f1f1orn I:domI1-1x𝒫VtxG|x=2I:domI1-1 ontoranI
6 4 5 syl GUSGraphI:domI1-1 ontoranI
7 edgval EdgG=raniEdgG
8 7 a1i GUSGraphEdgG=raniEdgG
9 1 eqcomi iEdgG=I
10 9 rneqi raniEdgG=ranI
11 8 10 eqtrdi GUSGraphEdgG=ranI
12 2 11 eqtrid GUSGraphE=ranI
13 12 f1oeq3d GUSGraphI:domI1-1 ontoEI:domI1-1 ontoranI
14 6 13 mpbird GUSGraphI:domI1-1 ontoE