frgrregord013 - Metamath Proof Explorer

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

Theorem frgrregord013 27141

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.

Step	Hyp	Ref	Expression
1		hashcl 13103	. . 3 ⊢ (𝑉 ∈ Fin → (#‘𝑉) ∈ ℕ₀)
2		ax-1 6	. . . . 5 ⊢ (((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ((((#‘𝑉) ∈ ℕ₀ ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
3		3ioran 1054	. . . . . 6 ⊢ (¬ ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3) ↔ (¬ (#‘𝑉) = 0 ∧ ¬ (#‘𝑉) = 1 ∧ ¬ (#‘𝑉) = 3))
4		df-ne 2791	. . . . . . . . . . . . 13 ⊢ ((#‘𝑉) ≠ 0 ↔ ¬ (#‘𝑉) = 0)
5		hasheq0 13110	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑉 ∈ Fin → ((#‘𝑉) = 0 ↔ 𝑉 = ∅))
6	5	necon3bid 2834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ Fin → ((#‘𝑉) ≠ 0 ↔ 𝑉 ≠ ∅))
7	6	biimpa 501	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → 𝑉 ≠ ∅)
8		elnnne0 11266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝑉) ∈ ℕ ↔ ((#‘𝑉) ∈ ℕ₀ ∧ (#‘𝑉) ≠ 0))
9		df-ne 2791	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((#‘𝑉) ≠ 1 ↔ ¬ (#‘𝑉) = 1)
10		eluz2b3 11722	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑉) ∈ (ℤ_≥‘2) ↔ ((#‘𝑉) ∈ ℕ ∧ (#‘𝑉) ≠ 1))
11		hash2prde 13206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 2) → ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))
12		vex 3193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑎 ∈ V
13	12	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑎 ≠ 𝑏 → 𝑎 ∈ V)
14		vex 3193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑏 ∈ V
15	14	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑎 ≠ 𝑏 → 𝑏 ∈ V)
16		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑎 ≠ 𝑏 → 𝑎 ≠ 𝑏)
17	13, 15, 16	3jca 1240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑎 ≠ 𝑏 → (𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏))
18		frgrreggt1.v	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑉 = (Vtx‘𝐺)
19	18	eqeq1i 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑉 = {𝑎, 𝑏} ↔ (Vtx‘𝐺) = {𝑎, 𝑏})
20	19	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑉 = {𝑎, 𝑏} → (Vtx‘𝐺) = {𝑎, 𝑏})
21		nfrgr2v 27034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏) ∧ (Vtx‘𝐺) = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph )
22	17, 20, 21	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph )
23		df-nel 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝐺 ∉ FriendGraph ↔ ¬ 𝐺 ∈ FriendGraph )
24	22, 23	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → ¬ 𝐺 ∈ FriendGraph )
25	24	pm2.21d 118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
26	25	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
27	26	exlimivv 1857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
28	11, 27	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 2) → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
29	28	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑉 ∈ Fin → ((#‘𝑉) = 2 → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
30	29	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ → ((#‘𝑉) = 2 → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
31	30	com14 96	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → ((#‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
32	31	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((#‘𝑉) ∈ (ℤ_≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → ((#‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
33	32	3imp 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑉) ∈ (ℤ_≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 2 → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
34	33	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((#‘𝑉) = 2 → (((#‘𝑉) ∈ (ℤ_≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
35		eqid 2621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (VtxDeg‘𝐺) = (VtxDeg‘𝐺)
36	18, 35	rusgrprop0 26367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾))
37		eluz2gt1 11720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((#‘𝑉) ∈ (ℤ_≥‘2) → 1 < (#‘𝑉))
38	37	anim2i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝐺 ∈ FriendGraph ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → (𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)))
39	38	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((#‘𝑉) ∈ (ℤ_≥‘2) ∧ 𝐺 ∈ FriendGraph ) → (𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)))
40	18	vdgn0frgrv2 27057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉) → (1 < (#‘𝑉) → ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
41	40	impancom 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)) → (𝑣 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
42	41	ralrimiv 2961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)) → ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
43		eqeq2 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝐾 = 0 → (((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0))
44	43	ralbidv 2982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0))
45		r19.26 3059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
46		nne 2794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 ⊢ (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0)
47	46	bicomi 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (((VtxDeg‘𝐺)‘𝑣) = 0 ↔ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
48	47	anbi1i 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
49		ancom 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
50		pm3.24 925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ ¬ (((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
51	50	bifal 1494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥)
52	48, 49, 51	3bitri 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥)
53	52	ralbii 2976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ∀𝑣 ∈ 𝑉 ⊥)
54		r19.3rzv 4042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑉 ≠ ∅ → (⊥ ↔ ∀𝑣 ∈ 𝑉 ⊥))
55		falim 1495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (⊥ → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))
56	54, 55	syl6bir 244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ (𝑉 ≠ ∅ → (∀𝑣 ∈ 𝑉 ⊥ → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
57	56	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ⊥ → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
58	57	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (∀𝑣 ∈ 𝑉 ⊥ → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
59	53, 58	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
60	45, 59	sylbir 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
61	60	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
62	44, 61	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
63	62	com4t 93	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
64	39, 42, 63	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((#‘𝑉) ∈ (ℤ_≥‘2) ∧ 𝐺 ∈ FriendGraph ) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
65	64	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((#‘𝑉) ∈ (ℤ_≥‘2) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
66	65	com25 99	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((#‘𝑉) ∈ (ℤ_≥‘2) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
67	66	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (𝐺 ∈ FriendGraph → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
68	67	com15 101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
69	68	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
70	69	3ad2ant3 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
71	36, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ FriendGraph → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
72	71	impcom 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
73	72	impcom 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
74	18	frrusgrord 27096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))
75	74	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))
76		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝐾 = 2 → 𝐾 = 2)
77		oveq1 6622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝐾 = 2 → (𝐾 − 1) = (2 − 1))
78	76, 77	oveq12d 6633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝐾 = 2 → (𝐾 · (𝐾 − 1)) = (2 · (2 − 1)))
79	78	oveq1d 6630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = ((2 · (2 − 1)) + 1))
80		2m1e1 11095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (2 − 1) = 1
81	80	oveq2i 6626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (2 · (2 − 1)) = (2 · 1)
82		2t1e2 11136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (2 · 1) = 2
83	81, 82	eqtri 2643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (2 · (2 − 1)) = 2
84	83	oveq1i 6625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((2 · (2 − 1)) + 1) = (2 + 1)
85		2p1e3 11111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (2 + 1) = 3
86	84, 85	eqtri 2643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((2 · (2 − 1)) + 1) = 3
87	79, 86	syl6eq 2671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = 3)
88	87	eqeq2d 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐾 = 2 → ((#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1) ↔ (#‘𝑉) = 3))
89		pm2.21 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (¬ (#‘𝑉) = 3 → ((#‘𝑉) = 3 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
90	89	ad2antrr 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 3 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
91	90	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((#‘𝑉) = 3 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
92	88, 91	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐾 = 2 → ((#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1) → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
93	75, 92	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 2 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
94	18	frgrreg 27140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2)))
95	94	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))
96	73, 93, 95	mpjaod 396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
97	96	exp32 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
98	97	com34 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
99	98	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (((¬ (#‘𝑉) = 3 ∧ ¬ (#‘𝑉) = 2) ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
100	99	exp4c 635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ (#‘𝑉) = 3 → (¬ (#‘𝑉) = 2 → ((#‘𝑉) ∈ (ℤ_≥‘2) → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
101	100	com34 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ (#‘𝑉) = 3 → ((#‘𝑉) ∈ (ℤ_≥‘2) → (¬ (#‘𝑉) = 2 → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
102	101	com25 99	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ (ℤ_≥‘2) → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
103	102	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ (ℤ_≥‘2) → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
104	103	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → ((#‘𝑉) ∈ (ℤ_≥‘2) → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
105	104	com14 96	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((#‘𝑉) ∈ (ℤ_≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
106	105	3imp 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((#‘𝑉) ∈ (ℤ_≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 2 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
107	106	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ (#‘𝑉) = 2 → (((#‘𝑉) ∈ (ℤ_≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
108	34, 107	pm2.61i 176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((#‘𝑉) ∈ (ℤ_≥‘2) ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
109	108	3exp 1261	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑉) ∈ (ℤ_≥‘2) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
110	10, 109	sylbir 225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((#‘𝑉) ∈ ℕ ∧ (#‘𝑉) ≠ 1) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
111	110	ex 450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((#‘𝑉) ∈ ℕ → ((#‘𝑉) ≠ 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
112	9, 111	syl5bir 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((#‘𝑉) ∈ ℕ → (¬ (#‘𝑉) = 1 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
113	112	com25 99	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝑉) ∈ ℕ → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
114	8, 113	sylbir 225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((#‘𝑉) ∈ ℕ₀ ∧ (#‘𝑉) ≠ 0) → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
115	114	ex 450	. . . . . . . . . . . . . . . . . . 19 ⊢ ((#‘𝑉) ∈ ℕ₀ → ((#‘𝑉) ≠ 0 → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))))
116	115	com23 86	. . . . . . . . . . . . . . . . . 18 ⊢ ((#‘𝑉) ∈ ℕ₀ → (𝑉 ∈ Fin → ((#‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))))
117	116	impd 447	. . . . . . . . . . . . . . . . 17 ⊢ ((#‘𝑉) ∈ ℕ₀ → ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
118	117	com14 96	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ≠ ∅ → ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ ℕ₀ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
119	7, 118	mpcom 38	. . . . . . . . . . . . . . 15 ⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ ℕ₀ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))))
120	119	ex 450	. . . . . . . . . . . . . 14 ⊢ (𝑉 ∈ Fin → ((#‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → ((#‘𝑉) ∈ ℕ₀ → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
121	120	com14 96	. . . . . . . . . . . . 13 ⊢ ((#‘𝑉) ∈ ℕ₀ → ((#‘𝑉) ≠ 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
122	4, 121	syl5bir 233	. . . . . . . . . . . 12 ⊢ ((#‘𝑉) ∈ ℕ₀ → (¬ (#‘𝑉) = 0 → (𝐺 ∈ FriendGraph → (𝑉 ∈ Fin → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
123	122	com24 95	. . . . . . . . . . 11 ⊢ ((#‘𝑉) ∈ ℕ₀ → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (¬ (#‘𝑉) = 0 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))))
124	123	3imp 1254	. . . . . . . . . 10 ⊢ (((#‘𝑉) ∈ ℕ₀ ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (¬ (#‘𝑉) = 0 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
125	124	com25 99	. . . . . . . . 9 ⊢ (((#‘𝑉) ∈ ℕ₀ ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) → (𝐺 RegUSGraph 𝐾 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (¬ (#‘𝑉) = 0 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))))
126	125	imp 445	. . . . . . . 8 ⊢ ((((#‘𝑉) ∈ ℕ₀ ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → (¬ (#‘𝑉) = 0 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
127	126	com14 96	. . . . . . 7 ⊢ (¬ (#‘𝑉) = 0 → (¬ (#‘𝑉) = 1 → (¬ (#‘𝑉) = 3 → ((((#‘𝑉) ∈ ℕ₀ ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
128	127	3imp 1254	. . . . . 6 ⊢ ((¬ (#‘𝑉) = 0 ∧ ¬ (#‘𝑉) = 1 ∧ ¬ (#‘𝑉) = 3) → ((((#‘𝑉) ∈ ℕ₀ ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
129	3, 128	sylbi 207	. . . . 5 ⊢ (¬ ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ((((#‘𝑉) ∈ ℕ₀ ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
130	2, 129	pm2.61i 176	. . . 4 ⊢ ((((#‘𝑉) ∈ ℕ₀ ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))
131	130	3exp1 1280	. . 3 ⊢ ((#‘𝑉) ∈ ℕ₀ → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
132	1, 131	mpcom 38	. 2 ⊢ (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
133	132	3imp21 1274	1 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∨ wo 383 ∧ wa 384 ∨ w3o 1035 ∧ w3a 1036 = wceq 1480 ⊥wfal 1485 ∃wex 1701 ∈ wcel 1987 ≠ wne 2790 ∉ wnel 2893 ∀wral 2908 Vcvv 3190 ∅c0 3897 {cpr 4157 class class class wbr 4623 ‘cfv 5857 (class class class)co 6615 Fincfn 7915 0cc0 9896 1c1 9897 + caddc 9899 · cmul 9901 < clt 10034 − cmin 10226 ℕcn 10980 2c2 11030 3c3 11031 ℕ₀cn0 11252 ℕ₀^*cxnn0 11323 ℤ_≥cuz 11647 #chash 13073 Vtxcvtx 25808 USGraph cusgr 25971 VtxDegcvtxdg 26282 RegUSGraph crusgr 26356 FriendGraph cfrgr 27020

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-rep 4741 ax-sep 4751 ax-nul 4759 ax-pow 4813 ax-pr 4877 ax-un 6914 ax-inf2 8498 ax-ac2 9245 ax-cnex 9952 ax-resscn 9953 ax-1cn 9954 ax-icn 9955 ax-addcl 9956 ax-addrcl 9957 ax-mulcl 9958 ax-mulrcl 9959 ax-mulcom 9960 ax-addass 9961 ax-mulass 9962 ax-distr 9963 ax-i2m1 9964 ax-1ne0 9965 ax-1rid 9966 ax-rnegex 9967 ax-rrecex 9968 ax-cnre 9969 ax-pre-lttri 9970 ax-pre-lttrn 9971 ax-pre-ltadd 9972 ax-pre-mulgt0 9973 ax-pre-sup 9974

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-ifp 1012 df-3or 1037 df-3an 1038 df-tru 1483 df-fal 1486 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2913 df-rex 2914 df-reu 2915 df-rmo 2916 df-rab 2917 df-v 3192 df-sbc 3423 df-csb 3520 df-dif 3563 df-un 3565 df-in 3567 df-ss 3574 df-pss 3576 df-nul 3898 df-if 4065 df-pw 4138 df-sn 4156 df-pr 4158 df-tp 4160 df-op 4162 df-uni 4410 df-int 4448 df-iun 4494 df-disj 4594 df-br 4624 df-opab 4684 df-mpt 4685 df-tr 4723 df-eprel 4995 df-id 4999 df-po 5005 df-so 5006 df-fr 5043 df-se 5044 df-we 5045 df-xp 5090 df-rel 5091 df-cnv 5092 df-co 5093 df-dm 5094 df-rn 5095 df-res 5096 df-ima 5097 df-pred 5649 df-ord 5695 df-on 5696 df-lim 5697 df-suc 5698 df-iota 5820 df-fun 5859 df-fn 5860 df-f 5861 df-f1 5862 df-fo 5863 df-f1o 5864 df-fv 5865 df-isom 5866 df-riota 6576 df-ov 6618 df-oprab 6619 df-mpt2 6620 df-om 7028 df-1st 7128 df-2nd 7129 df-wrecs 7367 df-recs 7428 df-rdg 7466 df-1o 7520 df-2o 7521 df-oadd 7524 df-er 7702 df-ec 7704 df-qs 7708 df-map 7819 df-pm 7820 df-en 7916 df-dom 7917 df-sdom 7918 df-fin 7919 df-sup 8308 df-inf 8309 df-oi 8375 df-card 8725 df-ac 8899 df-cda 8950 df-pnf 10036 df-mnf 10037 df-xr 10038 df-ltxr 10039 df-le 10040 df-sub 10228 df-neg 10229 df-div 10645 df-nn 10981 df-2 11039 df-3 11040 df-n0 11253 df-xnn0 11324 df-z 11338 df-uz 11648 df-rp 11793 df-xadd 11907 df-ico 12139 df-fz 12285 df-fzo 12423 df-fl 12549 df-mod 12625 df-seq 12758 df-exp 12817 df-hash 13074 df-word 13254 df-lsw 13255 df-concat 13256 df-s1 13257 df-substr 13258 df-reps 13261 df-csh 13488 df-s2 13546 df-s3 13547 df-cj 13789 df-re 13790 df-im 13791 df-sqrt 13925 df-abs 13926 df-clim 14169 df-sum 14367 df-dvds 14927 df-gcd 15160 df-prm 15329 df-phi 15414 df-vtx 25810 df-iedg 25811 df-edg 25874 df-uhgr 25883 df-ushgr 25884 df-upgr 25907 df-umgr 25908 df-uspgr 25972 df-usgr 25973 df-fusgr 26131 df-nbgr 26149 df-vtxdg 26283 df-rgr 26357 df-rusgr 26358 df-wlks 26399 df-wlkson 26400 df-trls 26492 df-trlson 26493 df-pths 26515 df-spths 26516 df-pthson 26517 df-spthson 26518 df-wwlks 26625 df-wwlksn 26626 df-wwlksnon 26627 df-wspthsn 26628 df-wspthsnon 26629 df-clwwlks 26778 df-clwwlksn 26779 df-conngr 26947 df-frgr 27021

This theorem is referenced by: frgrregord13 27142

W3C validator