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