Metamath Proof Explorer

Theorem frgrregord013

Description: If a finite friendship graph is K-regular, then it must have order 0, 1 or 3. (Contributed by Alexander van der Vekens, 9-Oct-2018) (Revised by AV, 4-Jun-2021)

Ref Expression
Hypothesis frgrreggt1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion frgrregord013 ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) )

Proof

Step Hyp Ref Expression
1 frgrreggt1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 hashcl ⊢ ( 𝑉 ∈ Fin → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
3 ax-1 ⊢ ( ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) → ( ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
4 3ioran ⊢ ( ¬ ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ↔ ( ¬ ( ♯ ‘ 𝑉 ) = 0 ∧ ¬ ( ♯ ‘ 𝑉 ) = 1 ∧ ¬ ( ♯ ‘ 𝑉 ) = 3 ) )
5 df-ne ⊢ ( ( ♯ ‘ 𝑉 ) ≠ 0 ↔ ¬ ( ♯ ‘ 𝑉 ) = 0 )
6 hasheq0 ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) = 0 ↔ 𝑉 = ∅ ) )
7 6 necon3bid ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) ≠ 0 ↔ 𝑉 ≠ ∅ ) )
8 7 biimpa ⊢ ( ( 𝑉 ∈ Fin ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → 𝑉 ≠ ∅ )
9 elnnne0 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) )
10 df-ne ⊢ ( ( ♯ ‘ 𝑉 ) ≠ 1 ↔ ¬ ( ♯ ‘ 𝑉 ) = 1 )
11 eluz2b3 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( ♯ ‘ 𝑉 ) ∈ ℕ ∧ ( ♯ ‘ 𝑉 ) ≠ 1 ) )
12 hash2prde ⊢ ( ( 𝑉 ∈ Fin ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) )
13 vex ⊢ 𝑎 ∈ V
14 13 a1i ⊢ ( 𝑎 ≠ 𝑏 → 𝑎 ∈ V )
15 vex ⊢ 𝑏 ∈ V
16 15 a1i ⊢ ( 𝑎 ≠ 𝑏 → 𝑏 ∈ V )
17 id ⊢ ( 𝑎 ≠ 𝑏 → 𝑎 ≠ 𝑏 )
18 14 16 17 3jca ⊢ ( 𝑎 ≠ 𝑏 → ( 𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏 ) )
19 1 eqeq1i ⊢ ( 𝑉 = { 𝑎 , 𝑏 } ↔ ( Vtx ‘ 𝐺 ) = { 𝑎 , 𝑏 } )
20 19 biimpi ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( Vtx ‘ 𝐺 ) = { 𝑎 , 𝑏 } )
21 nfrgr2v ⊢ ( ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏 ) ∧ ( Vtx ‘ 𝐺 ) = { 𝑎 , 𝑏 } ) → 𝐺 ∉ FriendGraph )
22 18 20 21 syl2an ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → 𝐺 ∉ FriendGraph )
23 df-nel ⊢ ( 𝐺 ∉ FriendGraph ↔ ¬ 𝐺 ∈ FriendGraph )
24 22 23 sylib ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ¬ 𝐺 ∈ FriendGraph )
25 24 pm2.21d ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
26 25 com23 ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑉 ≠ ∅ → ( 𝐺 ∈ FriendGraph → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
27 26 exlimivv ⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑉 ≠ ∅ → ( 𝐺 ∈ FriendGraph → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
28 12 27 syl ⊢ ( ( 𝑉 ∈ Fin ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ( 𝑉 ≠ ∅ → ( 𝐺 ∈ FriendGraph → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
29 28 ex ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) = 2 → ( 𝑉 ≠ ∅ → ( 𝐺 ∈ FriendGraph → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) )
30 29 com23 ⊢ ( 𝑉 ∈ Fin → ( 𝑉 ≠ ∅ → ( ( ♯ ‘ 𝑉 ) = 2 → ( 𝐺 ∈ FriendGraph → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) )
31 30 com14 ⊢ ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( ( ♯ ‘ 𝑉 ) = 2 → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) )
32 31 a1i ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( ( ♯ ‘ 𝑉 ) = 2 → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
33 32 3imp ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) = 2 → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
34 33 com12 ⊢ ( ( ♯ ‘ 𝑉 ) = 2 → ( ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ) → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
35 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
36 1 35 rusgrprop0 ⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
37 eluz2gt1 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → 1 < ( ♯ ‘ 𝑉 ) )
38 37 anim1ci ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ FriendGraph ) → ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) )
39 1 vdgn0frgrv2 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) )
40 39 impancom ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 𝑣 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) )
41 40 ralrimiv ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 )
42 eqeq2 ⊢ ( 𝐾 = 0 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ) )
43 42 ralbidv ⊢ ( 𝐾 = 0 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ↔ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ) )
44 r19.26 ⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) ↔ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) )
45 nne ⊢ ( ¬ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 )
46 45 bicomi ⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ↔ ¬ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 )
47 46 anbi1i ⊢ ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) ↔ ( ¬ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) )
48 ancom ⊢ ( ( ¬ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) ↔ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ∧ ¬ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) )
49 pm3.24 ⊢ ¬ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ∧ ¬ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 )
50 49 bifal ⊢ ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ∧ ¬ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) ↔ ⊥ )
51 47 48 50 3bitri ⊢ ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) ↔ ⊥ )
52 51 ralbii ⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) ↔ ∀ 𝑣 ∈ 𝑉 ⊥ )
53 r19.3rzv ⊢ ( 𝑉 ≠ ∅ → ( ⊥ ↔ ∀ 𝑣 ∈ 𝑉 ⊥ ) )
54 falim ⊢ ( ⊥ → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) )
55 53 54 biimtrrdi ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑣 ∈ 𝑉 ⊥ → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
56 55 adantl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ⊥ → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
57 56 com12 ⊢ ( ∀ 𝑣 ∈ 𝑉 ⊥ → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
58 52 57 sylbi ⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ∧ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
59 44 58 sylbir ⊢ ( ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 ) → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
60 59 ex ⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) )
61 43 60 biimtrdi ⊢ ( 𝐾 = 0 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
62 61 com4t ⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ≠ 0 → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
63 38 41 62 3syl ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ FriendGraph ) → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
64 63 ex ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝐺 ∈ FriendGraph → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
65 64 com25 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
66 65 adantl ⊢ ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
67 66 com15 ⊢ ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
68 67 com12 ⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( 𝐺 ∈ FriendGraph → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
69 68 3ad2ant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐺 ∈ FriendGraph → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
70 36 69 syl ⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ FriendGraph → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
71 70 impcom ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐾 = 0 → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
72 71 impcom ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) )
73 1 frrusgrord ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) )
74 73 imp ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) )
75 id ⊢ ( 𝐾 = 2 → 𝐾 = 2 )
76 oveq1 ⊢ ( 𝐾 = 2 → ( 𝐾 − 1 ) = ( 2 − 1 ) )
77 75 76 oveq12d ⊢ ( 𝐾 = 2 → ( 𝐾 · ( 𝐾 − 1 ) ) = ( 2 · ( 2 − 1 ) ) )
78 77 oveq1d ⊢ ( 𝐾 = 2 → ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) = ( ( 2 · ( 2 − 1 ) ) + 1 ) )
79 2m1e1 ⊢ ( 2 − 1 ) = 1
80 79 oveq2i ⊢ ( 2 · ( 2 − 1 ) ) = ( 2 · 1 )
81 2t1e2 ⊢ ( 2 · 1 ) = 2
82 80 81 eqtri ⊢ ( 2 · ( 2 − 1 ) ) = 2
83 82 oveq1i ⊢ ( ( 2 · ( 2 − 1 ) ) + 1 ) = ( 2 + 1 )
84 2p1e3 ⊢ ( 2 + 1 ) = 3
85 83 84 eqtri ⊢ ( ( 2 · ( 2 − 1 ) ) + 1 ) = 3
86 78 85 eqtrdi ⊢ ( 𝐾 = 2 → ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) = 3 )
87 86 eqeq2d ⊢ ( 𝐾 = 2 → ( ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ↔ ( ♯ ‘ 𝑉 ) = 3 ) )
88 pm2.21 ⊢ ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( ( ♯ ‘ 𝑉 ) = 3 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
89 88 ad2antrr ⊢ ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 3 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
90 89 com12 ⊢ ( ( ♯ ‘ 𝑉 ) = 3 → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
91 87 90 biimtrdi ⊢ ( 𝐾 = 2 → ( ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) )
92 74 91 syl5com ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 2 → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) )
93 1 frgrreg ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) ) )
94 93 imp ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( 𝐾 = 0 ∨ 𝐾 = 2 ) )
95 72 92 94 mpjaod ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) ) → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
96 95 exp32 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ FriendGraph → ( 𝐺 RegUSGraph 𝐾 → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
97 96 com34 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ FriendGraph → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
98 97 com23 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( ( ¬ ( ♯ ‘ 𝑉 ) = 3 ∧ ¬ ( ♯ ‘ 𝑉 ) = 2 ) ∧ ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐺 ∈ FriendGraph → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
99 98 exp4c ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( ¬ ( ♯ ‘ 𝑉 ) = 2 → ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝐺 ∈ FriendGraph → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) )
100 99 com34 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( ¬ ( ♯ ‘ 𝑉 ) = 2 → ( 𝐺 ∈ FriendGraph → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) )
101 100 com25 ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( ¬ ( ♯ ‘ 𝑉 ) = 2 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) )
102 101 ex ⊢ ( 𝑉 ∈ Fin → ( 𝑉 ≠ ∅ → ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( ¬ ( ♯ ‘ 𝑉 ) = 2 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
103 102 com23 ⊢ ( 𝑉 ∈ Fin → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( ¬ ( ♯ ‘ 𝑉 ) = 2 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
104 103 com14 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 2 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
105 104 3imp ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ) → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 2 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
106 105 com3r ⊢ ( ¬ ( ♯ ‘ 𝑉 ) = 2 → ( ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ) → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
107 34 106 pm2.61i ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ) → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
108 107 3exp ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ( ℤ≥ ‘ 2 ) → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) )
109 11 108 sylbir ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ ∧ ( ♯ ‘ 𝑉 ) ≠ 1 ) → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) )
110 109 ex ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝑉 ) ≠ 1 → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
111 10 110 biimtrrid ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
112 111 com25 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( 𝑉 ∈ Fin → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
113 9 112 sylbir ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( 𝑉 ∈ Fin → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
114 113 ex ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑉 ) ≠ 0 → ( 𝑉 ∈ Fin → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) ) )
115 114 impcomd ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ( 𝑉 ∈ Fin ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( 𝐺 ∈ FriendGraph → ( 𝑉 ≠ ∅ → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
116 115 com14 ⊢ ( 𝑉 ≠ ∅ → ( ( 𝑉 ∈ Fin ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
117 8 116 mpcom ⊢ ( ( 𝑉 ∈ Fin ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) )
118 117 ex ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) ≠ 0 → ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
119 118 com14 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑉 ) ≠ 0 → ( 𝐺 ∈ FriendGraph → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
120 5 119 biimtrrid ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ¬ ( ♯ ‘ 𝑉 ) = 0 → ( 𝐺 ∈ FriendGraph → ( 𝑉 ∈ Fin → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
121 120 com24 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( 𝑉 ∈ Fin → ( 𝐺 ∈ FriendGraph → ( ¬ ( ♯ ‘ 𝑉 ) = 0 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) ) ) )
122 121 3imp ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → ( ¬ ( ♯ ‘ 𝑉 ) = 0 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
123 122 com25 ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → ( 𝐺 RegUSGraph 𝐾 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( ¬ ( ♯ ‘ 𝑉 ) = 0 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) ) )
124 123 imp ⊢ ( ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( ¬ ( ♯ ‘ 𝑉 ) = 0 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
125 124 com14 ⊢ ( ¬ ( ♯ ‘ 𝑉 ) = 0 → ( ¬ ( ♯ ‘ 𝑉 ) = 1 → ( ¬ ( ♯ ‘ 𝑉 ) = 3 → ( ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
126 125 3imp ⊢ ( ( ¬ ( ♯ ‘ 𝑉 ) = 0 ∧ ¬ ( ♯ ‘ 𝑉 ) = 1 ∧ ¬ ( ♯ ‘ 𝑉 ) = 3 ) → ( ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
127 4 126 sylbi ⊢ ( ¬ ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) → ( ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) )
128 3 127 pm2.61i ⊢ ( ( ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) )
129 128 3exp1 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( 𝑉 ∈ Fin → ( 𝐺 ∈ FriendGraph → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) ) )
130 2 129 mpcom ⊢ ( 𝑉 ∈ Fin → ( 𝐺 ∈ FriendGraph → ( 𝐺 RegUSGraph 𝐾 → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) ) ) )
131 130 3imp21 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( ♯ ‘ 𝑉 ) = 0 ∨ ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) )