# 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}=\mathrm{Vtx}\left({G}\right)$
frgrregorufr0.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
frgrregorufr0.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
Assertion frgrregorufr ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$

### Proof

Step Hyp Ref Expression
1 frgrregorufr0.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 frgrregorufr0.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 frgrregorufr0.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
4 1 2 3 frgrregorufr0 ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)\ne {K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)$
5 orc ${⊢}\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)$
6 5 a1d ${⊢}\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\to \left(\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
7 fveq2 ${⊢}{v}={a}\to {D}\left({v}\right)={D}\left({a}\right)$
8 7 neeq1d ${⊢}{v}={a}\to \left({D}\left({v}\right)\ne {K}↔{D}\left({a}\right)\ne {K}\right)$
9 8 rspcva ${⊢}\left({a}\in {V}\wedge \forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)\ne {K}\right)\to {D}\left({a}\right)\ne {K}$
10 df-ne ${⊢}{D}\left({a}\right)\ne {K}↔¬{D}\left({a}\right)={K}$
11 pm2.21 ${⊢}¬{D}\left({a}\right)={K}\to \left({D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
12 10 11 sylbi ${⊢}{D}\left({a}\right)\ne {K}\to \left({D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
13 9 12 syl ${⊢}\left({a}\in {V}\wedge \forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)\ne {K}\right)\to \left({D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
14 13 ancoms ${⊢}\left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)\ne {K}\wedge {a}\in {V}\right)\to \left({D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
15 14 rexlimdva ${⊢}\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)\ne {K}\to \left(\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
16 olc ${⊢}\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)$
17 16 a1d ${⊢}\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\to \left(\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
18 6 15 17 3jaoi ${⊢}\left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)\ne {K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\to \left(\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
19 4 18 syl ${⊢}{G}\in \mathrm{FriendGraph}\to \left(\exists {a}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({a}\right)={K}\to \left(\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{D}\left({v}\right)={K}\vee \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({V}\setminus \left\{{v}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$