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 → G NeighbVtx U ∈ 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 → ∃ f f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e
4 f1ofo ⊢ f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e → f : G NeighbVtx U ⟶ onto e ∈ E | U ∈ e
5 fofi ⊢ G NeighbVtx U ∈ Fin ∧ f : G NeighbVtx U ⟶ onto e ∈ E | U ∈ e → e ∈ E | U ∈ e ∈ Fin
6 5 expcom ⊢ f : G NeighbVtx U ⟶ onto e ∈ E | U ∈ e → G NeighbVtx U ∈ Fin → e ∈ E | U ∈ e ∈ Fin
7 4 6 syl ⊢ f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e → G NeighbVtx U ∈ Fin → e ∈ E | U ∈ e ∈ Fin
8 7 exlimiv ⊢ ∃ f f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e → G NeighbVtx U ∈ Fin → e ∈ E | U ∈ e ∈ Fin
9 3 8 syl ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U ∈ Fin → e ∈ E | U ∈ e ∈ Fin
10 f1of1 ⊢ f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e → f : G NeighbVtx U ⟶ 1-1 e ∈ E | U ∈ e
11 f1fi ⊢ e ∈ E | U ∈ e ∈ Fin ∧ f : G NeighbVtx U ⟶ 1-1 e ∈ E | U ∈ e → G NeighbVtx U ∈ Fin
12 11 expcom ⊢ f : G NeighbVtx U ⟶ 1-1 e ∈ E | U ∈ e → e ∈ E | U ∈ e ∈ Fin → G NeighbVtx U ∈ Fin
13 10 12 syl ⊢ f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e → e ∈ E | U ∈ e ∈ Fin → G NeighbVtx U ∈ Fin
14 13 exlimiv ⊢ ∃ f f : G NeighbVtx U ⟶ 1-1 onto e ∈ E | U ∈ e → e ∈ E | U ∈ e ∈ Fin → G NeighbVtx U ∈ Fin
15 3 14 syl ⊢ G ∈ USGraph ∧ U ∈ V → e ∈ E | U ∈ e ∈ Fin → G NeighbVtx U ∈ Fin
16 9 15 impbid ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U ∈ Fin ↔ e ∈ E | U ∈ e ∈ Fin