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 FinUSGraph N V e E | N e Fin

Proof

Step Hyp Ref Expression
1 fusgredgfi.v V = Vtx G
2 fusgredgfi.e E = Edg G
3 2 fvexi E V
4 rabexg E V e E | N e V
5 3 4 mp1i G FinUSGraph N V e E | N e V
6 1 isfusgr G FinUSGraph G USGraph V Fin
7 hashcl V Fin V 0
8 6 7 simplbiim G FinUSGraph V 0
9 8 adantr G FinUSGraph N V V 0
10 fusgrusgr G FinUSGraph G USGraph
11 1 2 usgredgleord G USGraph N V e E | N e V
12 10 11 sylan G FinUSGraph N V e E | N e V
13 hashbnd e E | N e V V 0 e E | N e V e E | N e Fin
14 5 9 12 13 syl3anc G FinUSGraph N V e E | N e Fin