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

Theorem frgrregord013 27237
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 13142 . . 3 (𝑉 ∈ Fin → (#‘𝑉) ∈ ℕ0)
2 ax-1 6 . . . . 5 (((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ((((#‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
3 3ioran 1055 . . . . . 6 (¬ ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3) ↔ (¬ (#‘𝑉) = 0 ∧ ¬ (#‘𝑉) = 1 ∧ ¬ (#‘𝑉) = 3))
4 df-ne 2794 . . . . . . . . . . . . 13 ((#‘𝑉) ≠ 0 ↔ ¬ (#‘𝑉) = 0)
5 hasheq0 13149 . . . . . . . . . . . . . . . . . 18 (𝑉 ∈ Fin → ((#‘𝑉) = 0 ↔ 𝑉 = ∅))
65necon3bid 2837 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ Fin → ((#‘𝑉) ≠ 0 ↔ 𝑉 ≠ ∅))
76biimpa 501 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → 𝑉 ≠ ∅)
8 elnnne0 11303 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝑉) ∈ ℕ ↔ ((#‘𝑉) ∈ ℕ0 ∧ (#‘𝑉) ≠ 0))
9 df-ne 2794 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑉) ≠ 1 ↔ ¬ (#‘𝑉) = 1)
10 eluz2b3 11759 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑉) ∈ (ℤ‘2) ↔ ((#‘𝑉) ∈ ℕ ∧ (#‘𝑉) ≠ 1))
11 hash2prde 13247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑉 ∈ Fin ∧ (#‘𝑉) = 2) → ∃𝑎𝑏(𝑎𝑏𝑉 = {𝑎, 𝑏}))
12 vex 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑎 ∈ V
1312a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑎𝑏𝑎 ∈ V)
14 vex 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑏 ∈ V
1514a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑎𝑏𝑏 ∈ V)
16 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑎𝑏𝑎𝑏)
1713, 15, 163jca 1241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏 → (𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎𝑏))
18 frgrreggt1.v . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑉 = (Vtx‘𝐺)
1918eqeq1i 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑉 = {𝑎, 𝑏} ↔ (Vtx‘𝐺) = {𝑎, 𝑏})
2019biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑉 = {𝑎, 𝑏} → (Vtx‘𝐺) = {𝑎, 𝑏})
21 nfrgr2v 27129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎𝑏) ∧ (Vtx‘𝐺) = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph )
2217, 20, 21syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎𝑏𝑉 = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph )
23 df-nel 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝐺 ∉ FriendGraph ↔ ¬ 𝐺 ∈ FriendGraph )
2422, 23sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎𝑏𝑉 = {𝑎, 𝑏}) → ¬ 𝐺 ∈ FriendGraph )
2524pm2.21d 118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑎𝑏𝑉 = {𝑎, 𝑏}) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
2625com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎𝑏𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
2726exlimivv 1859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑎𝑏(𝑎𝑏𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
2811, 27syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑉 ∈ Fin ∧ (#‘𝑉) = 2) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
2928ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑉 ∈ Fin → ((#‘𝑉) = 2 → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
3029com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑉 ∈ Fin → (𝑉 ≠ ∅ → ((#‘𝑉) = 2 → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
3130com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → ((#‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
3231a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → ((#‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
33323imp 1255 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
3433com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((#‘𝑉) = 2 → (((#‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
35 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (VtxDeg‘𝐺) = (VtxDeg‘𝐺)
3618, 35rusgrprop0 26457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾))
37 eluz2gt1 11757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((#‘𝑉) ∈ (ℤ‘2) → 1 < (#‘𝑉))
3837anim2i 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝐺 ∈ FriendGraph ∧ (#‘𝑉) ∈ (ℤ‘2)) → (𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)))
3938ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (((#‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ) → (𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)))
4018vdgn0frgrv2 27152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((𝐺 ∈ FriendGraph ∧ 𝑣𝑉) → (1 < (#‘𝑉) → ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
4140impancom 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)) → (𝑣𝑉 → ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
4241ralrimiv 2964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)) → ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
43 eqeq2 2632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 (𝐾 = 0 → (((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0))
4443ralbidv 2985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0))
45 r19.26 3062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (∀𝑣𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
46 nne 2797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0)
4746bicomi 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 (((VtxDeg‘𝐺)‘𝑣) = 0 ↔ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
4847anbi1i 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
49 ancom 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ((¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
50 pm3.24 926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ¬ (((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
5150bifal 1496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ((((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥)
5248, 49, 513bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥)
5352ralbii 2979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (∀𝑣𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ∀𝑣𝑉 ⊥)
54 r19.3rzv 4062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 (𝑉 ≠ ∅ → (⊥ ↔ ∀𝑣𝑉 ⊥))
55 falim 1497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 (⊥ → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))
5654, 55syl6bir 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 (𝑉 ≠ ∅ → (∀𝑣𝑉 ⊥ → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
5756adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣𝑉 ⊥ → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
5857com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 (∀𝑣𝑉 ⊥ → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
5953, 58sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 (∀𝑣𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
6045, 59sylbir 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ((∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
6160ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
6244, 61syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
6362com4t 93 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
6439, 42, 633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((#‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
6564ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((#‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
6665com25 99 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((#‘𝑉) ∈ (ℤ‘2) → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
6766adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
6867com15 101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐺 ∈ FriendGraph → (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
6968com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
70693ad2ant3 1083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
7136, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
7271impcom 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
7372impcom 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
7418frrusgrord 27192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))
7574imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))
76 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝐾 = 2 → 𝐾 = 2)
77 oveq1 6654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝐾 = 2 → (𝐾 − 1) = (2 − 1))
7876, 77oveq12d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐾 = 2 → (𝐾 · (𝐾 − 1)) = (2 · (2 − 1)))
7978oveq1d 6662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = ((2 · (2 − 1)) + 1))
80 2m1e1 11132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (2 − 1) = 1
8180oveq2i 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (2 · (2 − 1)) = (2 · 1)
82 2t1e2 11173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (2 · 1) = 2
8381, 82eqtri 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (2 · (2 − 1)) = 2
8483oveq1i 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((2 · (2 − 1)) + 1) = (2 + 1)
85 2p1e3 11148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (2 + 1) = 3
8684, 85eqtri 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((2 · (2 − 1)) + 1) = 3
8779, 86syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = 3)
8887eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐾 = 2 → ((#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1) ↔ (#‘𝑉) = 3))
89 pm2.21 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (¬ (#‘𝑉) = 3 → ((#‘𝑉) = 3 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
9089ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 3 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
9190com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((#‘𝑉) = 3 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
9288, 91syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐾 = 2 → ((#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1) → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
9375, 92syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 2 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
9418frgrreg 27236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2)))
9594imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))
9673, 93, 95mpjaod 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
9796exp32 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
9897com34 91 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
9998com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ‘2)) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
10099exp4c 636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ (#‘𝑉) = 3 → (¬ (#‘𝑉) = 2 → ((#‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
101100com34 91 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ (#‘𝑉) = 3 → ((#‘𝑉) ∈ (ℤ‘2) → (¬ (#‘𝑉) = 2 → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
102101com25 99 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ (ℤ‘2) → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
103102ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ (ℤ‘2) → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
104103com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → ((#‘𝑉) ∈ (ℤ‘2) → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
105104com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
1061053imp 1255 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
107106com3r 87 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ (#‘𝑉) = 2 → (((#‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
10834, 107pm2.61i 176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#‘𝑉) ∈ (ℤ‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
1091083exp 1263 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑉) ∈ (ℤ‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
11010, 109sylbir 225 . . . . . . . . . . . . . . . . . . . . . . . 24 (((#‘𝑉) ∈ ℕ ∧ (#‘𝑉) ≠ 1) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
111110ex 450 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑉) ∈ ℕ → ((#‘𝑉) ≠ 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
1129, 111syl5bir 233 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝑉) ∈ ℕ → (¬ (#‘𝑉) = 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
113112com25 99 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝑉) ∈ ℕ → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
1148, 113sylbir 225 . . . . . . . . . . . . . . . . . . . 20 (((#‘𝑉) ∈ ℕ0 ∧ (#‘𝑉) ≠ 0) → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
115114ex 450 . . . . . . . . . . . . . . . . . . 19 ((#‘𝑉) ∈ ℕ0 → ((#‘𝑉) ≠ 0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))))
116115com23 86 . . . . . . . . . . . . . . . . . 18 ((#‘𝑉) ∈ ℕ0 → (𝑉 ∈ Fin → ((#‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))))
117116impd 447 . . . . . . . . . . . . . . . . 17 ((#‘𝑉) ∈ ℕ0 → ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
118117com14 96 . . . . . . . . . . . . . . . 16 (𝑉 ≠ ∅ → ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ ℕ0 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
1197, 118mpcom 38 . . . . . . . . . . . . . . 15 ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ ℕ0 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
120119ex 450 . . . . . . . . . . . . . 14 (𝑉 ∈ Fin → ((#‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ ℕ0 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
121120com14 96 . . . . . . . . . . . . 13 ((#‘𝑉) ∈ ℕ0 → ((#‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
1224, 121syl5bir 233 . . . . . . . . . . . 12 ((#‘𝑉) ∈ ℕ0 → (¬ (#‘𝑉) = 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
123122com24 95 . . . . . . . . . . 11 ((#‘𝑉) ∈ ℕ0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 0 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
1241233imp 1255 . . . . . . . . . 10 (((#‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (¬ (#‘𝑉) = 0 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
125124com25 99 . . . . . . . . 9 (((#‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (𝐺 RegUSGraph 𝐾 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (¬ (#‘𝑉) = 0 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
126125imp 445 . . . . . . . 8 ((((#‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (¬ (#‘𝑉) = 0 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
127126com14 96 . . . . . . 7 (¬ (#‘𝑉) = 0 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → ((((#‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
1281273imp 1255 . . . . . 6 ((¬ (#‘𝑉) = 0 ∧ ¬ (#‘𝑉) = 1 ∧ ¬ (#‘𝑉) = 3) → ((((#‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
1293, 128sylbi 207 . . . . 5 (¬ ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ((((#‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
1302, 129pm2.61i 176 . . . 4 ((((#‘𝑉) ∈ ℕ0𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))
1311303exp1 1282 . . 3 ((#‘𝑉) ∈ ℕ0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
1321, 131mpcom 38 . 2 (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
1331323imp21 1276 1 ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384  w3o 1036  w3a 1037   = wceq 1482  wfal 1487  wex 1703  wcel 1989  wne 2793  wnel 2896  wral 2911  Vcvv 3198  c0 3913  {cpr 4177   class class class wbr 4651  cfv 5886  (class class class)co 6647  Fincfn 7952  0cc0 9933  1c1 9934   + caddc 9936   · cmul 9938   < clt 10071  cmin 10263  cn 11017  2c2 11067  3c3 11068  0cn0 11289  0*cxnn0 11360  cuz 11684  #chash 13112  Vtxcvtx 25868   USGraph cusgr 26038  VtxDegcvtxdg 26355   RegUSGraph crusgr 26446   FriendGraph cfrgr 27113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-inf2 8535  ax-ac2 9282  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1013  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-disj 4619  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-2o 7558  df-oadd 7561  df-er 7739  df-ec 7741  df-qs 7745  df-map 7856  df-pm 7857  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-sup 8345  df-inf 8346  df-oi 8412  df-card 8762  df-ac 8936  df-cda 8987  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-3 11077  df-n0 11290  df-xnn0 11361  df-z 11375  df-uz 11685  df-rp 11830  df-xadd 11944  df-ico 12178  df-fz 12324  df-fzo 12462  df-fl 12588  df-mod 12664  df-seq 12797  df-exp 12856  df-hash 13113  df-word 13294  df-lsw 13295  df-concat 13296  df-s1 13297  df-substr 13298  df-reps 13301  df-csh 13529  df-s2 13587  df-s3 13588  df-cj 13833  df-re 13834  df-im 13835  df-sqrt 13969  df-abs 13970  df-clim 14213  df-sum 14411  df-dvds 14978  df-gcd 15211  df-prm 15380  df-phi 15465  df-vtx 25870  df-iedg 25871  df-edg 25934  df-uhgr 25947  df-ushgr 25948  df-upgr 25971  df-umgr 25972  df-uspgr 26039  df-usgr 26040  df-fusgr 26203  df-nbgr 26222  df-vtxdg 26356  df-rgr 26447  df-rusgr 26448  df-wlks 26489  df-wlkson 26490  df-trls 26583  df-trlson 26584  df-pths 26606  df-spths 26607  df-pthson 26608  df-spthson 26609  df-wwlks 26716  df-wwlksn 26717  df-wwlksnon 26718  df-wspthsn 26719  df-wspthsnon 26720  df-clwwlks 26871  df-clwwlksn 26872  df-conngr 27040  df-frgr 27114
This theorem is referenced by:  frgrregord13  27238
  Copyright terms: Public domain W3C validator