Theorem usgriedgleord

Description: Alternate version of usgredgleord , not using the notation ( EdgG ) . 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)

	Ref	Expression
Hypotheses	usgredg2v.v	|- V = ( Vtx ` G )
	usgredg2v.e	|- E = ( iEdg ` G )
Assertion	usgriedgleord	|- ( ( G e. USGraph /\ N e. V ) -> ( # ` { x e. dom E | N e. ( E ` x ) } ) <_ ( # ` V ) )

Proof

Step	Hyp	Ref	Expression
1		usgredg2v.v	|- V = ( Vtx ` G )
2		usgredg2v.e	|- E = ( iEdg ` G )
3	1	fvexi	|- V e. _V
4		eqid	|- { x e. dom E | N e. ( E ` x ) } = { x e. dom E | N e. ( E ` x ) }
5		eqid	|- ( y e. { x e. dom E | N e. ( E ` x ) } |-> ( iota_ z e. V ( E ` y ) = { z , N } ) ) = ( y e. { x e. dom E | N e. ( E ` x ) } |-> ( iota_ z e. V ( E ` y ) = { z , N } ) )
6	1 2 4 5	usgredg2v	|- ( ( G e. USGraph /\ N e. V ) -> ( y e. { x e. dom E | N e. ( E ` x ) } |-> ( iota_ z e. V ( E ` y ) = { z , N } ) ) : { x e. dom E | N e. ( E ` x ) } -1-1-> V )
7		f1domg	|- ( V e. _V -> ( ( y e. { x e. dom E | N e. ( E ` x ) } |-> ( iota_ z e. V ( E ` y ) = { z , N } ) ) : { x e. dom E | N e. ( E ` x ) } -1-1-> V -> { x e. dom E | N e. ( E ` x ) } ~<_ V ) )
8	3 6 7	mpsyl	|- ( ( G e. USGraph /\ N e. V ) -> { x e. dom E | N e. ( E ` x ) } ~<_ V )
9		hashdomi	|- ( { x e. dom E | N e. ( E ` x ) } ~<_ V -> ( # ` { x e. dom E | N e. ( E ` x ) } ) <_ ( # ` V ) )
10	8 9	syl	|- ( ( G e. USGraph /\ N e. V ) -> ( # ` { x e. dom E | N e. ( E ` x ) } ) <_ ( # ` V ) )