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