Metamath Proof Explorer

Theorem frgrregorufr

Description: If there is a vertex having degree K for each (nonnegative integer) K in a friendship graph, then either all vertices have degree K or 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". (Contributed by Alexander van der Vekens, 1-Jan-2018)

Ref Expression
Hypotheses frgrregorufr0.v ⊢V=Vtx⁡G
frgrregorufr0.e ⊢E=Edg⁡G
frgrregorufr0.d ⊢D=VtxDeg⁡G
Assertion frgrregorufr ⊢G∈FriendGraph→∃a∈VD⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E

Proof

Step Hyp Ref Expression
1 frgrregorufr0.v ⊢V=Vtx⁡G
2 frgrregorufr0.e ⊢E=Edg⁡G
3 frgrregorufr0.d ⊢D=VtxDeg⁡G
4 1 2 3 frgrregorufr0 ⊢G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
5 orc ⊢∀v∈VD⁡v=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
6 5 a1d ⊢∀v∈VD⁡v=K→∃a∈VD⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
7 fveq2 ⊢v=a→D⁡v=D⁡a
8 7 neeq1d ⊢v=a→D⁡v≠K↔D⁡a≠K
9 8 rspcva ⊢a∈V∧∀v∈VD⁡v≠K→D⁡a≠K
10 df-ne ⊢D⁡a≠K↔¬D⁡a=K
11 pm2.21 ⊢¬D⁡a=K→D⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
12 10 11 sylbi ⊢D⁡a≠K→D⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
13 9 12 syl ⊢a∈V∧∀v∈VD⁡v≠K→D⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
14 13 ancoms ⊢∀v∈VD⁡v≠K∧a∈V→D⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
15 14 rexlimdva ⊢∀v∈VD⁡v≠K→∃a∈VD⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
16 olc ⊢∃v∈V∀w∈V∖vvw∈E→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
17 16 a1d ⊢∃v∈V∀w∈V∖vvw∈E→∃a∈VD⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
18 6 15 17 3jaoi ⊢∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E→∃a∈VD⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E
19 4 18 syl ⊢G∈FriendGraph→∃a∈VD⁡a=K→∀v∈VD⁡v=K∨∃v∈V∀w∈V∖vvw∈E