Metamath Proof Explorer


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 ) )