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 ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ 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 ∖ v v w ∈ E
9 8 3mix3d ⊢ G ∈ FriendGraph ∧ x ∈ V | D ⁡ x = K = 1 → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
10 9 expcom ⊢ x ∈ V | D ⁡ x = K = 1 → G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ 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 ∈ V D ⁡ v ≠ K
18 17 3mix2d ⊢ ∀ v ∈ V ¬ D ⁡ v = K → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
19 18 a1d ⊢ ∀ v ∈ V ¬ D ⁡ v = K → G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
20 15 19 sylbi ⊢ x ∈ V | D ⁡ x = K = ∅ → G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
21 10 20 jaoi ⊢ x ∈ V | D ⁡ x = K = 1 ∨ x ∈ V | D ⁡ x = K = ∅ → G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
22 1 3 5 6 2 frgrwopreg2 ⊢ G ∈ FriendGraph ∧ V ∖ x ∈ V | D ⁡ x = K = 1 → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
23 22 3mix3d ⊢ G ∈ FriendGraph ∧ V ∖ x ∈ V | D ⁡ x = K = 1 → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
24 23 expcom ⊢ V ∖ x ∈ V | D ⁡ x = K = 1 → G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ 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 ∈ V D ⁡ v = K
28 26 27 bitri ⊢ V = x ∈ V | D ⁡ x = K ↔ ∀ v ∈ V D ⁡ v = K
29 3mix1 ⊢ ∀ v ∈ V D ⁡ v = K → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
30 29 a1d ⊢ ∀ v ∈ V D ⁡ v = K → G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
31 28 30 sylbi ⊢ V = x ∈ V | D ⁡ x = K → G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
32 25 31 sylbi ⊢ V ∖ x ∈ V | D ⁡ x = K = ∅ → G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
33 24 32 jaoi ⊢ V ∖ x ∈ V | D ⁡ x = K = 1 ∨ V ∖ x ∈ V | D ⁡ x = K = ∅ → G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ 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 ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
35 7 34 mpcom ⊢ G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E