Metamath Proof Explorer

Theorem frusgrnn0

Description: In a nonempty finite k-regular simple graph, the degree of each vertex is finite. (Contributed by AV, 7-May-2021)

Ref Expression
Hypothesis frusgrnn0.v ⊢ V = Vtx ⁡ G
Assertion frusgrnn0 ⊢ G ∈ FinUSGraph ∧ G RegUSGraph K ∧ V ≠ ∅ → K ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 frusgrnn0.v ⊢ V = Vtx ⁡ G
2 3simpb ⊢ G ∈ FinUSGraph ∧ G RegUSGraph K ∧ V ≠ ∅ → G ∈ FinUSGraph ∧ V ≠ ∅
3 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
4 1 3 rusgrprop0 ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K
5 4 simp3d ⊢ G RegUSGraph K → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K
6 5 3ad2ant2 ⊢ G ∈ FinUSGraph ∧ G RegUSGraph K ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K
7 1 3 fusgrregdegfi ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → K ∈ ℕ 0
8 2 6 7 sylc ⊢ G ∈ FinUSGraph ∧ G RegUSGraph K ∧ V ≠ ∅ → K ∈ ℕ 0