Metamath Proof Explorer

Theorem friendship

Description: The friendship theorem: In every finite (nonempty) friendship graph there is a vertex which is adjacent to all other vertices. This is Metamath 100 proof #83. (Contributed by Alexander van der Vekens, 9-Oct-2018)

Ref Expression
Hypothesis friendship.v ⊢ V = Vtx ⁡ G
Assertion friendship ⊢ G ∈ FriendGraph ∧ V ≠ ∅ ∧ V ∈ Fin → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G

Proof

Step Hyp Ref Expression
1 friendship.v ⊢ V = Vtx ⁡ G
2 simpr1 ⊢ 3 < V ∧ G ∈ FriendGraph ∧ V ≠ ∅ ∧ V ∈ Fin → G ∈ FriendGraph
3 simpr3 ⊢ 3 < V ∧ G ∈ FriendGraph ∧ V ≠ ∅ ∧ V ∈ Fin → V ∈ Fin
4 simpl ⊢ 3 < V ∧ G ∈ FriendGraph ∧ V ≠ ∅ ∧ V ∈ Fin → 3 < V
5 1 friendshipgt3 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ 3 < V → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
6 2 3 4 5 syl3anc ⊢ 3 < V ∧ G ∈ FriendGraph ∧ V ≠ ∅ ∧ V ∈ Fin → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
7 6 ex ⊢ 3 < V → G ∈ FriendGraph ∧ V ≠ ∅ ∧ V ∈ Fin → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
8 hashcl ⊢ V ∈ Fin → V ∈ ℕ 0
9 simplr ⊢ V ∈ ℕ 0 ∧ V ∈ Fin ∧ ¬ 3 < V ∧ V ≠ ∅ → V ∈ Fin
10 hashge1 ⊢ V ∈ Fin ∧ V ≠ ∅ → 1 ≤ V
11 10 ad2ant2l ⊢ V ∈ ℕ 0 ∧ V ∈ Fin ∧ ¬ 3 < V ∧ V ≠ ∅ → 1 ≤ V
12 nn0re ⊢ V ∈ ℕ 0 → V ∈ ℝ
13 3re ⊢ 3 ∈ ℝ
14 lenlt ⊢ V ∈ ℝ ∧ 3 ∈ ℝ → V ≤ 3 ↔ ¬ 3 < V
15 12 13 14 sylancl ⊢ V ∈ ℕ 0 → V ≤ 3 ↔ ¬ 3 < V
16 15 biimprd ⊢ V ∈ ℕ 0 → ¬ 3 < V → V ≤ 3
17 16 adantr ⊢ V ∈ ℕ 0 ∧ V ∈ Fin → ¬ 3 < V → V ≤ 3
18 17 com12 ⊢ ¬ 3 < V → V ∈ ℕ 0 ∧ V ∈ Fin → V ≤ 3
19 18 adantr ⊢ ¬ 3 < V ∧ V ≠ ∅ → V ∈ ℕ 0 ∧ V ∈ Fin → V ≤ 3
20 19 impcom ⊢ V ∈ ℕ 0 ∧ V ∈ Fin ∧ ¬ 3 < V ∧ V ≠ ∅ → V ≤ 3
21 9 11 20 3jca ⊢ V ∈ ℕ 0 ∧ V ∈ Fin ∧ ¬ 3 < V ∧ V ≠ ∅ → V ∈ Fin ∧ 1 ≤ V ∧ V ≤ 3
22 21 exp31 ⊢ V ∈ ℕ 0 → V ∈ Fin → ¬ 3 < V ∧ V ≠ ∅ → V ∈ Fin ∧ 1 ≤ V ∧ V ≤ 3
23 8 22 mpcom ⊢ V ∈ Fin → ¬ 3 < V ∧ V ≠ ∅ → V ∈ Fin ∧ 1 ≤ V ∧ V ≤ 3
24 23 impcom ⊢ ¬ 3 < V ∧ V ≠ ∅ ∧ V ∈ Fin → V ∈ Fin ∧ 1 ≤ V ∧ V ≤ 3
25 hash1to3 ⊢ V ∈ Fin ∧ 1 ≤ V ∧ V ≤ 3 → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
26 vex ⊢ a ∈ V
27 eqid ⊢ Edg ⁡ G = Edg ⁡ G
28 1 27 1to3vfriendship ⊢ a ∈ V ∧ V = a ∨ V = a b ∨ V = a b c → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
29 26 28 mpan ⊢ V = a ∨ V = a b ∨ V = a b c → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
30 29 exlimiv ⊢ ∃ c V = a ∨ V = a b ∨ V = a b c → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
31 30 exlimivv ⊢ ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
32 24 25 31 3syl ⊢ ¬ 3 < V ∧ V ≠ ∅ ∧ V ∈ Fin → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
33 32 exp31 ⊢ ¬ 3 < V → V ≠ ∅ → V ∈ Fin → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
34 33 com14 ⊢ G ∈ FriendGraph → V ≠ ∅ → V ∈ Fin → ¬ 3 < V → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
35 34 3imp ⊢ G ∈ FriendGraph ∧ V ≠ ∅ ∧ V ∈ Fin → ¬ 3 < V → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
36 35 com12 ⊢ ¬ 3 < V → G ∈ FriendGraph ∧ V ≠ ∅ ∧ V ∈ Fin → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G
37 7 36 pm2.61i ⊢ G ∈ FriendGraph ∧ V ≠ ∅ ∧ V ∈ Fin → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ Edg ⁡ G