Metamath Proof Explorer

Theorem fusgrn0degnn0

Description: In a nonempty, finite graph there is a vertex having a nonnegative integer as degree. (Contributed by Alexander van der Vekens, 6-Sep-2018) (Revised by AV, 1-Apr-2021)

Ref Expression
Hypothesis fusgrn0degnn0.v ⊢ V = Vtx ⁡ G
Assertion fusgrn0degnn0 ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n

Proof

Step Hyp Ref Expression
1 fusgrn0degnn0.v ⊢ V = Vtx ⁡ G
2 n0 ⊢ V ≠ ∅ ↔ ∃ k k ∈ V
3 1 vtxdgfusgr ⊢ G ∈ FinUSGraph → ∀ u ∈ V VtxDeg ⁡ G ⁡ u ∈ ℕ 0
4 fveq2 ⊢ u = k → VtxDeg ⁡ G ⁡ u = VtxDeg ⁡ G ⁡ k
5 4 eleq1d ⊢ u = k → VtxDeg ⁡ G ⁡ u ∈ ℕ 0 ↔ VtxDeg ⁡ G ⁡ k ∈ ℕ 0
6 5 rspcv ⊢ k ∈ V → ∀ u ∈ V VtxDeg ⁡ G ⁡ u ∈ ℕ 0 → VtxDeg ⁡ G ⁡ k ∈ ℕ 0
7 risset ⊢ VtxDeg ⁡ G ⁡ k ∈ ℕ 0 ↔ ∃ n ∈ ℕ 0 n = VtxDeg ⁡ G ⁡ k
8 fveqeq2 ⊢ v = k → VtxDeg ⁡ G ⁡ v = n ↔ VtxDeg ⁡ G ⁡ k = n
9 eqcom ⊢ VtxDeg ⁡ G ⁡ k = n ↔ n = VtxDeg ⁡ G ⁡ k
10 8 9 bitrdi ⊢ v = k → VtxDeg ⁡ G ⁡ v = n ↔ n = VtxDeg ⁡ G ⁡ k
11 10 rexbidv ⊢ v = k → ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n ↔ ∃ n ∈ ℕ 0 n = VtxDeg ⁡ G ⁡ k
12 11 rspcev ⊢ k ∈ V ∧ ∃ n ∈ ℕ 0 n = VtxDeg ⁡ G ⁡ k → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n
13 12 expcom ⊢ ∃ n ∈ ℕ 0 n = VtxDeg ⁡ G ⁡ k → k ∈ V → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n
14 7 13 sylbi ⊢ VtxDeg ⁡ G ⁡ k ∈ ℕ 0 → k ∈ V → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n
15 14 com12 ⊢ k ∈ V → VtxDeg ⁡ G ⁡ k ∈ ℕ 0 → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n
16 6 15 syld ⊢ k ∈ V → ∀ u ∈ V VtxDeg ⁡ G ⁡ u ∈ ℕ 0 → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n
17 3 16 syl5 ⊢ k ∈ V → G ∈ FinUSGraph → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n
18 17 exlimiv ⊢ ∃ k k ∈ V → G ∈ FinUSGraph → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n
19 2 18 sylbi ⊢ V ≠ ∅ → G ∈ FinUSGraph → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n
20 19 impcom ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → ∃ v ∈ V ∃ n ∈ ℕ 0 VtxDeg ⁡ G ⁡ v = n