Metamath Proof Explorer

Theorem edgusgrnbfin

Description: The number of neighbors of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 28-Oct-2020)

Ref Expression
Hypotheses nbusgrf1o.v ⊢V=Vtx⁡G
nbusgrf1o.e ⊢E=Edg⁡G
Assertion edgusgrnbfin ⊢G∈USGraph∧U∈V→GNeighbVtxU∈Fin↔e∈E|U∈e∈Fin

Proof

Step Hyp Ref Expression
1 nbusgrf1o.v ⊢V=Vtx⁡G
2 nbusgrf1o.e ⊢E=Edg⁡G
3 1 2 nbusgrf1o ⊢G∈USGraph∧U∈V→∃ff:GNeighbVtxU⟶1-1 ontoe∈E|U∈e
4 f1ofo ⊢f:GNeighbVtxU⟶1-1 ontoe∈E|U∈e→f:GNeighbVtxU⟶ontoe∈E|U∈e
5 fofi ⊢GNeighbVtxU∈Fin∧f:GNeighbVtxU⟶ontoe∈E|U∈e→e∈E|U∈e∈Fin
6 5 expcom ⊢f:GNeighbVtxU⟶ontoe∈E|U∈e→GNeighbVtxU∈Fin→e∈E|U∈e∈Fin
7 4 6 syl ⊢f:GNeighbVtxU⟶1-1 ontoe∈E|U∈e→GNeighbVtxU∈Fin→e∈E|U∈e∈Fin
8 7 exlimiv ⊢∃ff:GNeighbVtxU⟶1-1 ontoe∈E|U∈e→GNeighbVtxU∈Fin→e∈E|U∈e∈Fin
9 3 8 syl ⊢G∈USGraph∧U∈V→GNeighbVtxU∈Fin→e∈E|U∈e∈Fin
10 f1of1 ⊢f:GNeighbVtxU⟶1-1 ontoe∈E|U∈e→f:GNeighbVtxU⟶1-1e∈E|U∈e
11 f1fi ⊢e∈E|U∈e∈Fin∧f:GNeighbVtxU⟶1-1e∈E|U∈e→GNeighbVtxU∈Fin
12 11 expcom ⊢f:GNeighbVtxU⟶1-1e∈E|U∈e→e∈E|U∈e∈Fin→GNeighbVtxU∈Fin
13 10 12 syl ⊢f:GNeighbVtxU⟶1-1 ontoe∈E|U∈e→e∈E|U∈e∈Fin→GNeighbVtxU∈Fin
14 13 exlimiv ⊢∃ff:GNeighbVtxU⟶1-1 ontoe∈E|U∈e→e∈E|U∈e∈Fin→GNeighbVtxU∈Fin
15 3 14 syl ⊢G∈USGraph∧U∈V→e∈E|U∈e∈Fin→GNeighbVtxU∈Fin
16 9 15 impbid ⊢G∈USGraph∧U∈V→GNeighbVtxU∈Fin↔e∈E|U∈e∈Fin