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

Metamath Proof Explorer

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