Metamath Proof Explorer

Theorem fusgrregdegfi

Description: In a nonempty finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018) (Revised by AV, 19-Dec-2020)

Ref Expression
Hypotheses isrusgr0.v ⊢ V = Vtx ⁡ G
isrusgr0.d ⊢ D = VtxDeg ⁡ G
Assertion fusgrregdegfi ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → ∀ v ∈ V D ⁡ v = K → K ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 isrusgr0.v ⊢ V = Vtx ⁡ G
2 isrusgr0.d ⊢ D = VtxDeg ⁡ G
3 1 vtxdgfusgr ⊢ G ∈ FinUSGraph → ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0
4 r19.26 ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0 ∧ D ⁡ v = K ↔ ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0 ∧ ∀ v ∈ V D ⁡ v = K
5 2 fveq1i ⊢ D ⁡ v = VtxDeg ⁡ G ⁡ v
6 5 eqeq1i ⊢ D ⁡ v = K ↔ VtxDeg ⁡ G ⁡ v = K
7 eleq1 ⊢ VtxDeg ⁡ G ⁡ v = K → VtxDeg ⁡ G ⁡ v ∈ ℕ 0 ↔ K ∈ ℕ 0
8 6 7 sylbi ⊢ D ⁡ v = K → VtxDeg ⁡ G ⁡ v ∈ ℕ 0 ↔ K ∈ ℕ 0
9 8 biimpac ⊢ VtxDeg ⁡ G ⁡ v ∈ ℕ 0 ∧ D ⁡ v = K → K ∈ ℕ 0
10 9 ralimi ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0 ∧ D ⁡ v = K → ∀ v ∈ V K ∈ ℕ 0
11 rspn0 ⊢ V ≠ ∅ → ∀ v ∈ V K ∈ ℕ 0 → K ∈ ℕ 0
12 10 11 syl5com ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0 ∧ D ⁡ v = K → V ≠ ∅ → K ∈ ℕ 0
13 4 12 sylbir ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0 ∧ ∀ v ∈ V D ⁡ v = K → V ≠ ∅ → K ∈ ℕ 0
14 13 ex ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0 → ∀ v ∈ V D ⁡ v = K → V ≠ ∅ → K ∈ ℕ 0
15 14 com23 ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0 → V ≠ ∅ → ∀ v ∈ V D ⁡ v = K → K ∈ ℕ 0
16 3 15 syl ⊢ G ∈ FinUSGraph → V ≠ ∅ → ∀ v ∈ V D ⁡ v = K → K ∈ ℕ 0
17 16 imp ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → ∀ v ∈ V D ⁡ v = K → K ∈ ℕ 0