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

Metamath Proof Explorer

Theorem fusgredgfi

Description: In a finite simple graph the number of edges which contain a given vertex is also finite. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 21-Oct-2020)

Ref Expression
Hypotheses fusgredgfi.v 
|- V = ( Vtx ` G )
fusgredgfi.e 
|- E = ( Edg ` G )
Assertion fusgredgfi 
|- ( ( G e. FinUSGraph /\ N e. V ) -> { e e. E | N e. e } e. Fin )

Proof

Step Hyp Ref Expression
1 fusgredgfi.v 
 |-  V = ( Vtx ` G )
2 fusgredgfi.e 
 |-  E = ( Edg ` G )
3 2 fvexi 
 |-  E e. _V
4 rabexg 
 |-  ( E e. _V -> { e e. E | N e. e } e. _V )
5 3 4 mp1i 
 |-  ( ( G e. FinUSGraph /\ N e. V ) -> { e e. E | N e. e } e. _V )
6 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
7 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
8 6 7 simplbiim 
 |-  ( G e. FinUSGraph -> ( # ` V ) e. NN0 )
9 8 adantr 
 |-  ( ( G e. FinUSGraph /\ N e. V ) -> ( # ` V ) e. NN0 )
10 fusgrusgr 
 |-  ( G e. FinUSGraph -> G e. USGraph )
11 1 2 usgredgleord 
 |-  ( ( G e. USGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )
12 10 11 sylan 
 |-  ( ( G e. FinUSGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )
13 hashbnd 
 |-  ( ( { e e. E | N e. e } e. _V /\ ( # ` V ) e. NN0 /\ ( # ` { e e. E | N e. e } ) <_ ( # ` V ) ) -> { e e. E | N e. e } e. Fin )
14 5 9 12 13 syl3anc 
 |-  ( ( G e. FinUSGraph /\ N e. V ) -> { e e. E | N e. e } e. Fin )