Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  frgrregord013 Structured version   Visualization version   GIF version

Theorem frgrregord013 28224
 Description: If a finite friendship graph is 𝐾-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.)
Hypothesis
Ref Expression
frgrreggt1.v 𝑉 = (Vtx‘𝐺)
Assertion
Ref Expression
frgrregord013 ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))

Proof of Theorem frgrregord013
Dummy variables 𝑣 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hashcl 13733 . . 3 (𝑉 ∈ Fin → (♯‘𝑉) ∈ ℕ0)
2 ax-1 6 . . . . 5 (((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3) → ((((♯‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
3 3ioran 1103 . . . . . 6 (¬ ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3) ↔ (¬ (♯‘𝑉) = 0 ∧ ¬ (♯‘𝑉) = 1 ∧ ¬ (♯‘𝑉) = 3))
4 df-ne 2988 . . . . . . . . . . . . 13 ((♯‘𝑉) ≠ 0 ↔ ¬ (♯‘𝑉) = 0)
5 hasheq0 13740 . . . . . . . . . . . . . . . . . 18 (𝑉 ∈ Fin → ((♯‘𝑉) = 0 ↔ 𝑉 = ∅))
65necon3bid 3031 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ Fin → ((♯‘𝑉) ≠ 0 ↔ 𝑉 ≠ ∅))
76biimpa 480 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ Fin ∧ (♯‘𝑉) ≠ 0) → 𝑉 ≠ ∅)
8 elnnne0 11917 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝑉) ∈ ℕ ↔ ((♯‘𝑉) ∈ ℕ0 ∧ (♯‘𝑉) ≠ 0))
9 df-ne 2988 . . . . . . . . . . . . . . . . . . . . . 22 ((♯‘𝑉) ≠ 1 ↔ ¬ (♯‘𝑉) = 1)
10 eluz2b3 12330 . . . . . . . . . . . . . . . . . . . . . . . 24 ((♯‘𝑉) ∈ (ℤ‘2) ↔ ((♯‘𝑉) ∈ ℕ ∧ (♯‘𝑉) ≠ 1))
11 hash2prde 13844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑉 ∈ Fin ∧ (♯‘𝑉) = 2) → ∃𝑎𝑏(𝑎𝑏𝑉 = {𝑎, 𝑏}))
12 vex 3445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 𝑎 ∈ V
1312a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏𝑎 ∈ V)
14 vex 3445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 𝑏 ∈ V
1514a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏𝑏 ∈ V)
16 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏𝑎𝑏)
1713, 15, 163jca 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑎𝑏 → (𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎𝑏))
18 frgrreggt1.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 𝑉 = (Vtx‘𝐺)
1918eqeq1i 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑉 = {𝑎, 𝑏} ↔ (Vtx‘𝐺) = {𝑎, 𝑏})
2019biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑉 = {𝑎, 𝑏} → (Vtx‘𝐺) = {𝑎, 𝑏})
21 nfrgr2v 28101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎𝑏) ∧ (Vtx‘𝐺) = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph )
2217, 20, 21syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎𝑏𝑉 = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph )
23 df-nel 3092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐺 ∉ FriendGraph ↔ ¬ 𝐺 ∈ FriendGraph )
2422, 23sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎𝑏𝑉 = {𝑎, 𝑏}) → ¬ 𝐺 ∈ FriendGraph )
2524pm2.21d 121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎𝑏𝑉 = {𝑎, 𝑏}) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
2625com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑎𝑏𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
2726exlimivv 1933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∃𝑎𝑏(𝑎𝑏𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
2811, 27syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑉 ∈ Fin ∧ (♯‘𝑉) = 2) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
2928ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑉 ∈ Fin → ((♯‘𝑉) = 2 → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))
3029com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑉 ∈ Fin → (𝑉 ≠ ∅ → ((♯‘𝑉) = 2 → (𝐺 ∈ FriendGraph → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))
3130com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → ((♯‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))
3231a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((♯‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → ((♯‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
33323imp 1108 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
3433com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((♯‘𝑉) = 2 → (((♯‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
35 eqid 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (VtxDeg‘𝐺) = (VtxDeg‘𝐺)
3618, 35rusgrprop0 27401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾))
37 eluz2gt1 12328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((♯‘𝑉) ∈ (ℤ‘2) → 1 < (♯‘𝑉))
3837anim1ci 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((♯‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ) → (𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)))
3918vdgn0frgrv2 28124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝐺 ∈ FriendGraph ∧ 𝑣𝑉) → (1 < (♯‘𝑉) → ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
4039impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → (𝑣𝑉 → ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
4140ralrimiv 3148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
42 eqeq2 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝐾 = 0 → (((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0))
4342ralbidv 3162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0))
44 r19.26 3137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (∀𝑣𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
45 nne 2991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0)
4645bicomi 227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 (((VtxDeg‘𝐺)‘𝑣) = 0 ↔ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
4746anbi1i 626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
48 ancom 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
49 pm3.24 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ¬ (((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
5049bifal 1554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥)
5147, 48, 503bitri 300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥)
5251ralbii 3133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (∀𝑣𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ∀𝑣𝑉 ⊥)
53 r19.3rzv 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 (𝑉 ≠ ∅ → (⊥ ↔ ∀𝑣𝑉 ⊥))
54 falim 1555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 (⊥ → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))
5553, 54syl6bir 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 (𝑉 ≠ ∅ → (∀𝑣𝑉 ⊥ → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
5655adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣𝑉 ⊥ → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
5756com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (∀𝑣𝑉 ⊥ → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
5852, 57sylbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (∀𝑣𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
5944, 58sylbir 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
6059ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))
6143, 60syl6bi 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
6261com4t 93 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
6338, 41, 623syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((♯‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
6463ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((♯‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
6564com25 99 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((♯‘𝑉) ∈ (ℤ‘2) → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
6665adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
6766com15 101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐺 ∈ FriendGraph → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
6867com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
69683ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
7036, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
7170impcom 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
7271impcom 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))
7318frrusgrord 28170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))
7473imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))
75 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐾 = 2 → 𝐾 = 2)
76 oveq1 7152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐾 = 2 → (𝐾 − 1) = (2 − 1))
7775, 76oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐾 = 2 → (𝐾 · (𝐾 − 1)) = (2 · (2 − 1)))
7877oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = ((2 · (2 − 1)) + 1))
79 2m1e1 11769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (2 − 1) = 1
8079oveq2i 7156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (2 · (2 − 1)) = (2 · 1)
81 2t1e2 11806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (2 · 1) = 2
8280, 81eqtri 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (2 · (2 − 1)) = 2
8382oveq1i 7155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((2 · (2 − 1)) + 1) = (2 + 1)
84 2p1e3 11785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (2 + 1) = 3
8583, 84eqtri 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((2 · (2 − 1)) + 1) = 3
8678, 85eqtrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = 3)
8786eqeq2d 2809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐾 = 2 → ((♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1) ↔ (♯‘𝑉) = 3))
88 pm2.21 123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (¬ (♯‘𝑉) = 3 → ((♯‘𝑉) = 3 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
8988ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 3 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
9089com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((♯‘𝑉) = 3 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
9187, 90syl6bi 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝐾 = 2 → ((♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1) → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))
9274, 91syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 2 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))
9318frgrreg 28223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2)))
9493imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))
9572, 92, 94mpjaod 857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
9695exp32 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
9796com34 91 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
9897com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (((¬ (♯‘𝑉) = 3 ∧ ¬ (♯‘𝑉) = 2) ∧ (♯‘𝑉) ∈ (ℤ‘2)) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
9998exp4c 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ (♯‘𝑉) = 3 → (¬ (♯‘𝑉) = 2 → ((♯‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))
10099com34 91 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ (♯‘𝑉) = 3 → ((♯‘𝑉) ∈ (ℤ‘2) → (¬ (♯‘𝑉) = 2 → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))
101100com25 99 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph → ((♯‘𝑉) ∈ (ℤ‘2) → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))
102101ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → ((♯‘𝑉) ∈ (ℤ‘2) → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
103102com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → ((♯‘𝑉) ∈ (ℤ‘2) → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
104103com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((♯‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
1051043imp 1108 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 2 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
106105com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (¬ (♯‘𝑉) = 2 → (((♯‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
10734, 106pm2.61i 185 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((♯‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
1081073exp 1116 . . . . . . . . . . . . . . . . . . . . . . . 24 ((♯‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))
10910, 108sylbir 238 . . . . . . . . . . . . . . . . . . . . . . 23 (((♯‘𝑉) ∈ ℕ ∧ (♯‘𝑉) ≠ 1) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))
110109ex 416 . . . . . . . . . . . . . . . . . . . . . 22 ((♯‘𝑉) ∈ ℕ → ((♯‘𝑉) ≠ 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
1119, 110syl5bir 246 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝑉) ∈ ℕ → (¬ (♯‘𝑉) = 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
112111com25 99 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝑉) ∈ ℕ → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
1138, 112sylbir 238 . . . . . . . . . . . . . . . . . . 19 (((♯‘𝑉) ∈ ℕ0 ∧ (♯‘𝑉) ≠ 0) → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
114113ex 416 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑉) ∈ ℕ0 → ((♯‘𝑉) ≠ 0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))))
115114impcomd 415 . . . . . . . . . . . . . . . . 17 ((♯‘𝑉) ∈ ℕ0 → ((𝑉 ∈ Fin ∧ (♯‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
116115com14 96 . . . . . . . . . . . . . . . 16 (𝑉 ≠ ∅ → ((𝑉 ∈ Fin ∧ (♯‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph → ((♯‘𝑉) ∈ ℕ0 → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
1177, 116mpcom 38 . . . . . . . . . . . . . . 15 ((𝑉 ∈ Fin ∧ (♯‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph → ((♯‘𝑉) ∈ ℕ0 → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))))
118117ex 416 . . . . . . . . . . . . . 14 (𝑉 ∈ Fin → ((♯‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → ((♯‘𝑉) ∈ ℕ0 → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
119118com14 96 . . . . . . . . . . . . 13 ((♯‘𝑉) ∈ ℕ0 → ((♯‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
1204, 119syl5bir 246 . . . . . . . . . . . 12 ((♯‘𝑉) ∈ ℕ0 → (¬ (♯‘𝑉) = 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
121120com24 95 . . . . . . . . . . 11 ((♯‘𝑉) ∈ ℕ0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (¬ (♯‘𝑉) = 0 → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))))
1221213imp 1108 . . . . . . . . . 10 (((♯‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (¬ (♯‘𝑉) = 0 → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
123122com25 99 . . . . . . . . 9 (((♯‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (𝐺 RegUSGraph 𝐾 → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (¬ (♯‘𝑉) = 0 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))))
124123imp 410 . . . . . . . 8 ((((♯‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → (¬ (♯‘𝑉) = 0 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
125124com14 96 . . . . . . 7 (¬ (♯‘𝑉) = 0 → (¬ (♯‘𝑉) = 1 → (¬ (♯‘𝑉) = 3 → ((((♯‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
1261253imp 1108 . . . . . 6 ((¬ (♯‘𝑉) = 0 ∧ ¬ (♯‘𝑉) = 1 ∧ ¬ (♯‘𝑉) = 3) → ((((♯‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
1273, 126sylbi 220 . . . . 5 (¬ ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3) → ((((♯‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))
1282, 127pm2.61i 185 . . . 4 ((((♯‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))
1291283exp1 1349 . . 3 ((♯‘𝑉) ∈ ℕ0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3)))))
1301, 129mpcom 38 . 2 (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))))
1311303imp21 1111 1 ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → ((♯‘𝑉) = 0 ∨ (♯‘𝑉) = 1 ∨ (♯‘𝑉) = 3))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 844   ∨ w3o 1083   ∧ w3a 1084   = wceq 1538  ⊥wfal 1550  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987   ∉ wnel 3091  ∀wral 3106  Vcvv 3442  ∅c0 4246  {cpr 4530   class class class wbr 5034  ‘cfv 6332  (class class class)co 7145  Fincfn 8510  0cc0 10544  1c1 10545   + caddc 10547   · cmul 10549   < clt 10682   − cmin 10877  ℕcn 11643  2c2 11698  3c3 11699  ℕ0cn0 11903  ℕ0*cxnn0 11975  ℤ≥cuz 12251  ♯chash 13706  Vtxcvtx 26833  USGraphcusgr 26986  VtxDegcvtxdg 27299   RegUSGraph crusgr 27390   FriendGraph cfrgr 28087 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-inf2 9106  ax-ac2 9892  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621  ax-pre-sup 10622 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ifp 1059  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-disj 5000  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-2o 8104  df-oadd 8107  df-er 8290  df-ec 8292  df-qs 8296  df-map 8409  df-pm 8410  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-sup 8908  df-inf 8909  df-oi 8976  df-dju 9332  df-card 9370  df-ac 9545  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-div 11305  df-nn 11644  df-2 11706  df-3 11707  df-n0 11904  df-xnn0 11976  df-z 11990  df-uz 12252  df-rp 12398  df-xadd 12516  df-ico 12752  df-fz 12906  df-fzo 13049  df-fl 13177  df-mod 13253  df-seq 13385  df-exp 13446  df-hash 13707  df-word 13878  df-lsw 13926  df-concat 13934  df-s1 13961  df-substr 14014  df-pfx 14044  df-reps 14142  df-csh 14162  df-s2 14221  df-s3 14222  df-cj 14470  df-re 14471  df-im 14472  df-sqrt 14606  df-abs 14607  df-clim 14857  df-sum 15055  df-dvds 15620  df-gcd 15854  df-prm 16026  df-phi 16113  df-vtx 26835  df-iedg 26836  df-edg 26885  df-uhgr 26895  df-ushgr 26896  df-upgr 26919  df-umgr 26920  df-uspgr 26987  df-usgr 26988  df-fusgr 27151  df-nbgr 27167  df-vtxdg 27300  df-rgr 27391  df-rusgr 27392  df-wlks 27433  df-wlkson 27434  df-trls 27526  df-trlson 27527  df-pths 27549  df-spths 27550  df-pthson 27551  df-spthson 27552  df-wwlks 27660  df-wwlksn 27661  df-wwlksnon 27662  df-wspthsn 27663  df-wspthsnon 27664  df-clwwlk 27811  df-clwwlkn 27854  df-clwwlknon 27917  df-conngr 28016  df-frgr 28088 This theorem is referenced by:  frgrregord13  28225
 Copyright terms: Public domain W3C validator