Metamath Proof Explorer


Theorem usgredgedg

Description: In a simple graph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 18-Oct-2020) (Proof shortened by AV, 11-Dec-2020)

Ref Expression
Hypotheses ushgredgedg.e E=EdgG
ushgredgedg.i I=iEdgG
ushgredgedg.v V=VtxG
ushgredgedg.a A=idomI|NIi
ushgredgedg.b B=eE|Ne
ushgredgedg.f F=xAIx
Assertion usgredgedg GUSGraphNVF:A1-1 ontoB

Proof

Step Hyp Ref Expression
1 ushgredgedg.e E=EdgG
2 ushgredgedg.i I=iEdgG
3 ushgredgedg.v V=VtxG
4 ushgredgedg.a A=idomI|NIi
5 ushgredgedg.b B=eE|Ne
6 ushgredgedg.f F=xAIx
7 usgruspgr GUSGraphGUSHGraph
8 uspgrushgr GUSHGraphGUSHGraph
9 7 8 syl GUSGraphGUSHGraph
10 1 2 3 4 5 6 ushgredgedg GUSHGraphNVF:A1-1 ontoB
11 9 10 sylan GUSGraphNVF:A1-1 ontoB