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 ∈ V D ⁡ a = 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 1 2 3 frgrregorufr0 ⊢ G ∈ FriendGraph → ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
5 orc ⊢ ∀ v ∈ V D ⁡ v = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
6 5 a1d ⊢ ∀ v ∈ V D ⁡ v = K → ∃ a ∈ V D ⁡ a = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ 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 ∈ V D ⁡ v ≠ K → D ⁡ a ≠ K
10 df-ne ⊢ D ⁡ a ≠ K ↔ ¬ D ⁡ a = K
11 pm2.21 ⊢ ¬ D ⁡ a = K → D ⁡ a = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
12 10 11 sylbi ⊢ D ⁡ a ≠ K → D ⁡ a = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
13 9 12 syl ⊢ a ∈ V ∧ ∀ v ∈ V D ⁡ v ≠ K → D ⁡ a = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
14 13 ancoms ⊢ ∀ v ∈ V D ⁡ v ≠ K ∧ a ∈ V → D ⁡ a = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
15 14 rexlimdva ⊢ ∀ v ∈ V D ⁡ v ≠ K → ∃ a ∈ V D ⁡ a = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
16 olc ⊢ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
17 16 a1d ⊢ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E → ∃ a ∈ V D ⁡ a = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
18 6 15 17 3jaoi ⊢ ∀ v ∈ V D ⁡ v = K ∨ ∀ v ∈ V D ⁡ v ≠ K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E → ∃ a ∈ V D ⁡ a = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
19 4 18 syl ⊢ G ∈ FriendGraph → ∃ a ∈ V D ⁡ a = K → ∀ v ∈ V D ⁡ v = K ∨ ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E