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 e. dom I | N e. ( I ` i ) }
	ushgredgedg.b	|- B = { e e. E | N e. e }
	ushgredgedg.f	|- F = ( x e. A |-> ( I ` x ) )
Assertion	usgredgedg	|- ( ( G e. USGraph /\ N e. 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 e. dom I | N e. ( I ` i ) }
5		ushgredgedg.b	|- B = { e e. E | N e. e }
6		ushgredgedg.f	|- F = ( x e. A |-> ( I ` x ) )
7		usgruspgr	|- ( G e. USGraph -> G e. USPGraph )
8		uspgrushgr	|- ( G e. USPGraph -> G e. USHGraph )
9	7 8	syl	|- ( G e. USGraph -> G e. USHGraph )
10	1 2 3 4 5 6	ushgredgedg	|- ( ( G e. USHGraph /\ N e. V ) -> F : A -1-1-onto-> B )
11	9 10	sylan	|- ( ( G e. USGraph /\ N e. V ) -> F : A -1-1-onto-> B )