Metamath Proof Explorer

Theorem frgrregorufrg

Description: If there is a vertex having degree k for each nonnegative integer k in a friendship graph, then there is a universal friend. This corresponds to claim 2 in Huneke p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". Variant of frgrregorufr with generalization. (Contributed by Alexander van der Vekens, 6-Sep-2018) (Revised by AV, 26-May-2021) (Proof shortened by AV, 12-Jan-2022)

Ref Expression
Hypotheses frgrregorufrg.v ⊢ V = Vtx ⁡ G
frgrregorufrg.e ⊢ E = Edg ⁡ G
Assertion frgrregorufrg ⊢ G ∈ FriendGraph → ∀ k ∈ ℕ 0 ∃ a ∈ V VtxDeg ⁡ G ⁡ a = k → G RegUSGraph k ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E

Proof

Step Hyp Ref Expression
1 frgrregorufrg.v ⊢ V = Vtx ⁡ G
2 frgrregorufrg.e ⊢ E = Edg ⁡ G
3 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
4 1 2 3 frgrregorufr ⊢ G ∈ FriendGraph → ∃ a ∈ V VtxDeg ⁡ G ⁡ a = k → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = k ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
5 4 adantr ⊢ G ∈ FriendGraph ∧ k ∈ ℕ 0 → ∃ a ∈ V VtxDeg ⁡ G ⁡ a = k → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = k ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
6 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
7 nn0xnn0 ⊢ k ∈ ℕ 0 → k ∈ ℕ 0 *
8 1 3 usgreqdrusgr ⊢ G ∈ USGraph ∧ k ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = k → G RegUSGraph k
9 8 3expia ⊢ G ∈ USGraph ∧ k ∈ ℕ 0 * → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = k → G RegUSGraph k
10 6 7 9 syl2an ⊢ G ∈ FriendGraph ∧ k ∈ ℕ 0 → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = k → G RegUSGraph k
11 10 orim1d ⊢ G ∈ FriendGraph ∧ k ∈ ℕ 0 → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = k ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E → G RegUSGraph k ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
12 5 11 syld ⊢ G ∈ FriendGraph ∧ k ∈ ℕ 0 → ∃ a ∈ V VtxDeg ⁡ G ⁡ a = k → G RegUSGraph k ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
13 12 ralrimiva ⊢ G ∈ FriendGraph → ∀ k ∈ ℕ 0 ∃ a ∈ V VtxDeg ⁡ G ⁡ a = k → G RegUSGraph k ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E