Metamath Proof Explorer

Theorem frgrregorufr0

Description: In a friendship graph there are either no vertices having degree K , or all vertices have degree K for any (nonnegative integer) K , unless there is a universal friend. This corresponds to claim 2 in Huneke p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1-Jan-2018) (Revised by AV, 11-May-2021) (Proof shortened by AV, 3-Jan-2022)

Ref Expression
Hypotheses frgrregorufr0.v ⊢V=Vtx⁡G
frgrregorufr0.e ⊢E=Edg⁡G
frgrregorufr0.d ⊢D=VtxDeg⁡G
Assertion frgrregorufr0 ⊢G∈FriendGraph→∀v∈VD⁡v=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 fveqeq2 ⊢x=y→D⁡x=K↔D⁡y=K
5 4 cbvrabv ⊢x∈V|D⁡x=K=y∈V|D⁡y=K
6 eqid ⊢V∖x∈V|D⁡x=K=V∖x∈V|D⁡x=K
7 1 3 5 6 frgrwopreg ⊢G∈FriendGraph→x∈V|D⁡x=K=1∨x∈V|D⁡x=K=∅∨V∖x∈V|D⁡x=K=1∨V∖x∈V|D⁡x=K=∅
8 1 3 5 6 2 frgrwopreg1 ⊢G∈FriendGraph∧x∈V|D⁡x=K=1→∃v∈V∀w∈V∖vvw∈E
9 8 3mix3d ⊢G∈FriendGraph∧x∈V|D⁡x=K=1→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
10 9 expcom ⊢x∈V|D⁡x=K=1→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
11 fveqeq2 ⊢x=v→D⁡x=K↔D⁡v=K
12 11 cbvrabv ⊢x∈V|D⁡x=K=v∈V|D⁡v=K
13 12 eqeq1i ⊢x∈V|D⁡x=K=∅↔v∈V|D⁡v=K=∅
14 rabeq0 ⊢v∈V|D⁡v=K=∅↔∀v∈V¬D⁡v=K
15 13 14 bitri ⊢x∈V|D⁡x=K=∅↔∀v∈V¬D⁡v=K
16 neqne ⊢¬D⁡v=K→D⁡v≠K
17 16 ralimi ⊢∀v∈V¬D⁡v=K→∀v∈VD⁡v≠K
18 17 3mix2d ⊢∀v∈V¬D⁡v=K→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
19 18 a1d ⊢∀v∈V¬D⁡v=K→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
20 15 19 sylbi ⊢x∈V|D⁡x=K=∅→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
21 10 20 jaoi ⊢x∈V|D⁡x=K=1∨x∈V|D⁡x=K=∅→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
22 1 3 5 6 2 frgrwopreg2 ⊢G∈FriendGraph∧V∖x∈V|D⁡x=K=1→∃v∈V∀w∈V∖vvw∈E
23 22 3mix3d ⊢G∈FriendGraph∧V∖x∈V|D⁡x=K=1→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
24 23 expcom ⊢V∖x∈V|D⁡x=K=1→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
25 difrab0eq ⊢V∖x∈V|D⁡x=K=∅↔V=x∈V|D⁡x=K
26 12 eqeq2i ⊢V=x∈V|D⁡x=K↔V=v∈V|D⁡v=K
27 rabid2 ⊢V=v∈V|D⁡v=K↔∀v∈VD⁡v=K
28 26 27 bitri ⊢V=x∈V|D⁡x=K↔∀v∈VD⁡v=K
29 3mix1 ⊢∀v∈VD⁡v=K→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
30 29 a1d ⊢∀v∈VD⁡v=K→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
31 28 30 sylbi ⊢V=x∈V|D⁡x=K→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
32 25 31 sylbi ⊢V∖x∈V|D⁡x=K=∅→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
33 24 32 jaoi ⊢V∖x∈V|D⁡x=K=1∨V∖x∈V|D⁡x=K=∅→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
34 21 33 jaoi ⊢x∈V|D⁡x=K=1∨x∈V|D⁡x=K=∅∨V∖x∈V|D⁡x=K=1∨V∖x∈V|D⁡x=K=∅→G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E
35 7 34 mpcom ⊢G∈FriendGraph→∀v∈VD⁡v=K∨∀v∈VD⁡v≠K∨∃v∈V∀w∈V∖vvw∈E