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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion friendship ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) )

Proof

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