This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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