Theorem usgredgleordALT

Description: Alternate proof for usgredgleord based on usgriedgleord . In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020) (Proof shortened by AV, 5-May-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	usgredgleord.v	|- V = ( Vtx ` G )
	usgredgleord.e	|- E = ( Edg ` G )
Assertion	usgredgleordALT	|- ( ( G e. USGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )

Proof

Step	Hyp	Ref	Expression
1		usgredgleord.v	|- V = ( Vtx ` G )
2		usgredgleord.e	|- E = ( Edg ` G )
3		fvex	|- ( iEdg ` G ) e. _V
4	3	dmex	|- dom ( iEdg ` G ) e. _V
5	4	rabex	|- { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } e. _V
6	5	a1i	|- ( ( G e. USGraph /\ N e. V ) -> { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } e. _V )
7		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
8		eqid	|- { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } = { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) }
9		eleq2w	|- ( e = f -> ( N e. e <-> N e. f ) )
10	9	cbvrabv	|- { e e. E | N e. e } = { f e. E | N e. f }
11		eqid	|- ( y e. { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } |-> ( ( iEdg ` G ) ` y ) ) = ( y e. { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } |-> ( ( iEdg ` G ) ` y ) )
12	2 7 1 8 10 11	usgredgedg	|- ( ( G e. USGraph /\ N e. V ) -> ( y e. { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } |-> ( ( iEdg ` G ) ` y ) ) : { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } -1-1-onto-> { e e. E | N e. e } )
13	6 12	hasheqf1od	|- ( ( G e. USGraph /\ N e. V ) -> ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) = ( # ` { e e. E | N e. e } ) )
14	1 7	usgriedgleord	|- ( ( G e. USGraph /\ N e. V ) -> ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) <_ ( # ` V ) )
15	13 14	eqbrtrrd	|- ( ( G e. USGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )