Metamath Proof Explorer

Theorem friendshipgt3

Description: The friendship theorem for big graphs: In every finite friendship graph with order greater than 3 there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 9-Oct-2018) (Revised by AV, 4-Jun-2021)

Ref Expression
Hypothesis frgrreggt1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion friendshipgt3 ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 frgrreggt1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 frgrregorufrg ⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) )
4 3 3ad2ant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) )
5 1 frgrogt3nreg ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 )
6 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
7 6 anim1i ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
8 1 isfusgr ⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) )
9 7 8 sylibr ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph )
10 9 3adant3 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → 𝐺 ∈ FinUSGraph )
11 0red ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → 0 ∈ ℝ )
12 3re ⊢ 3 ∈ ℝ
13 12 a1i ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → 3 ∈ ℝ )
14 hashcl ⊢ ( 𝑉 ∈ Fin → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
15 14 nn0red ⊢ ( 𝑉 ∈ Fin → ( ♯ ‘ 𝑉 ) ∈ ℝ )
16 15 adantr ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ( ♯ ‘ 𝑉 ) ∈ ℝ )
17 3pos ⊢ 0 < 3
18 17 a1i ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → 0 < 3 )
19 simpr ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → 3 < ( ♯ ‘ 𝑉 ) )
20 11 13 16 18 19 lttrd ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → 0 < ( ♯ ‘ 𝑉 ) )
21 20 gt0ne0d ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ( ♯ ‘ 𝑉 ) ≠ 0 )
22 hasheq0 ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) = 0 ↔ 𝑉 = ∅ ) )
23 22 adantr ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ↔ 𝑉 = ∅ ) )
24 23 necon3bid ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ( ( ♯ ‘ 𝑉 ) ≠ 0 ↔ 𝑉 ≠ ∅ ) )
25 21 24 mpbid ⊢ ( ( 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → 𝑉 ≠ ∅ )
26 25 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → 𝑉 ≠ ∅ )
27 1 fusgrn0degnn0 ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ∃ 𝑡 ∈ 𝑉 ∃ 𝑚 ∈ ℕ0 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 )
28 10 26 27 syl2anc ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑡 ∈ 𝑉 ∃ 𝑚 ∈ ℕ0 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 )
29 r19.26 ⊢ ( ∀ 𝑘 ∈ ℕ0 ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑘 ) ↔ ( ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ∀ 𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 ) )
30 simpllr ⊢ ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) → 𝑚 ∈ ℕ0 )
31 fveqeq2 ⊢ ( 𝑢 = 𝑡 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) )
32 31 rspcev ⊢ ( ( 𝑡 ∈ 𝑉 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) → ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 )
33 32 ad4ant13 ⊢ ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) → ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 )
34 ornld ⊢ ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 → ( ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 → ( 𝐺 RegUSGraph 𝑚 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑚 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) )
35 33 34 syl ⊢ ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) → ( ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 → ( 𝐺 RegUSGraph 𝑚 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑚 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) )
36 35 adantr ⊢ ( ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) ∧ 𝑘 = 𝑚 ) → ( ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 → ( 𝐺 RegUSGraph 𝑚 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑚 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) )
37 eqeq2 ⊢ ( 𝑘 = 𝑚 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 ) )
38 37 rexbidv ⊢ ( 𝑘 = 𝑚 → ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 ↔ ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 ) )
39 breq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐺 RegUSGraph 𝑘 ↔ 𝐺 RegUSGraph 𝑚 ) )
40 39 orbi1d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝐺 RegUSGraph 𝑚 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) )
41 38 40 imbi12d ⊢ ( 𝑘 = 𝑚 → ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 → ( 𝐺 RegUSGraph 𝑚 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
42 39 notbid ⊢ ( 𝑘 = 𝑚 → ( ¬ 𝐺 RegUSGraph 𝑘 ↔ ¬ 𝐺 RegUSGraph 𝑚 ) )
43 41 42 anbi12d ⊢ ( 𝑘 = 𝑚 → ( ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑘 ) ↔ ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 → ( 𝐺 RegUSGraph 𝑚 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑚 ) ) )
44 43 imbi1d ⊢ ( 𝑘 = 𝑚 → ( ( ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑘 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 → ( 𝐺 RegUSGraph 𝑚 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑚 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) )
45 44 adantl ⊢ ( ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) ∧ 𝑘 = 𝑚 ) → ( ( ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑘 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑚 → ( 𝐺 RegUSGraph 𝑚 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑚 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) )
46 36 45 mpbird ⊢ ( ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) ∧ 𝑘 = 𝑚 ) → ( ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑘 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) )
47 30 46 rspcimdv ⊢ ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) → ( ∀ 𝑘 ∈ ℕ0 ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑘 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) )
48 47 com12 ⊢ ( ∀ 𝑘 ∈ ℕ0 ( ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ¬ 𝐺 RegUSGraph 𝑘 ) → ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) )
49 29 48 sylbir ⊢ ( ( ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ∀ 𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 ) → ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) )
50 49 expcom ⊢ ( ∀ 𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ( ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) )
51 50 com13 ⊢ ( ( ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) ) → ( ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ∀ 𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) )
52 51 exp31 ⊢ ( ( 𝑡 ∈ 𝑉 ∧ 𝑚 ∈ ℕ0 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 → ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ( ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ∀ 𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ) ) )
53 52 rexlimivv ⊢ ( ∃ 𝑡 ∈ 𝑉 ∃ 𝑚 ∈ ℕ0 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑡 ) = 𝑚 → ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ( ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ∀ 𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
54 28 53 mpcom ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ( ∀ 𝑘 ∈ ℕ0 ( ∃ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) = 𝑘 → ( 𝐺 RegUSGraph 𝑘 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ∀ 𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) ) ) )
55 4 5 54 mp2d ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ ( Edg ‘ 𝐺 ) )