Theorem uspgredgleord

Description: In a simple pseudograph 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, 6-Dec-2020)

	Ref	Expression
Hypotheses	usgredgleord.v	|- V = ( Vtx ` G )
	usgredgleord.e	|- E = ( Edg ` G )
Assertion	uspgredgleord	|- ( ( G e. USPGraph /\ 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	1	fvexi	|- V e. _V
4		eqid	|- { e e. E | N e. e } = { e e. E | N e. e }
5		eqid	|- ( x e. { e e. E | N e. e } |-> ( iota_ y e. V x = { N , y } ) ) = ( x e. { e e. E | N e. e } |-> ( iota_ y e. V x = { N , y } ) )
6	1 2 4 5	uspgredg2v	|- ( ( G e. USPGraph /\ N e. V ) -> ( x e. { e e. E | N e. e } |-> ( iota_ y e. V x = { N , y } ) ) : { e e. E | N e. e } -1-1-> V )
7		f1domg	|- ( V e. _V -> ( ( x e. { e e. E | N e. e } |-> ( iota_ y e. V x = { N , y } ) ) : { e e. E | N e. e } -1-1-> V -> { e e. E | N e. e } ~<_ V ) )
8	3 6 7	mpsyl	|- ( ( G e. USPGraph /\ N e. V ) -> { e e. E | N e. e } ~<_ V )
9		hashdomi	|- ( { e e. E | N e. e } ~<_ V -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )
10	8 9	syl	|- ( ( G e. USPGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )