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 )