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 = Edg G
ushgredgedg.i I = iEdg G
ushgredgedg.v V = Vtx G
ushgredgedg.a A = i dom I | N I i
ushgredgedg.b B = e E | N e
ushgredgedg.f F = x A I x
Assertion usgredgedg G USGraph N V F : A 1-1 onto B

Proof

Step Hyp Ref Expression
1 ushgredgedg.e E = Edg G
2 ushgredgedg.i I = iEdg G
3 ushgredgedg.v V = Vtx G
4 ushgredgedg.a A = i dom I | N I i
5 ushgredgedg.b B = e E | N e
6 ushgredgedg.f F = x A I x
7 usgruspgr G USGraph G USHGraph
8 uspgrushgr G USHGraph G USHGraph
9 7 8 syl G USGraph G USHGraph
10 1 2 3 4 5 6 ushgredgedg G USHGraph N V F : A 1-1 onto B
11 9 10 sylan G USGraph N V F : A 1-1 onto B