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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion fusgrn0degnn0 ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ∃ 𝑣 ∈ 𝑉 ∃ 𝑛 ∈ ℕ0 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑛 )

Proof

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