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 27253

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 13147	. . 3 ⊢ (𝑉 ∈ Fin → (#‘𝑉) ∈ ℕ₀)
2		ax-1 6	. . . . 5 ⊢ (((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ((((#‘𝑉) ∈ ℕ₀ ∧ 𝑉 ∈ Fin ∧ 𝐺 ∈ FriendGraph ) ∧ 𝐺 RegUSGraph 𝐾) → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
3		3ioran 1056	. . . . . 6 ⊢ (¬ ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3) ↔ (¬ (#‘𝑉) = 0 ∧ ¬ (#‘𝑉) = 1 ∧ ¬ (#‘𝑉) = 3))
4		df-ne 2795	. . . . . . . . . . . . 13 ⊢ ((#‘𝑉) ≠ 0 ↔ ¬ (#‘𝑉) = 0)
5		hasheq0 13154	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑉 ∈ Fin → ((#‘𝑉) = 0 ↔ 𝑉 = ∅))
6	5	necon3bid 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝑉 ∈ Fin → ((#‘𝑉) ≠ 0 ↔ 𝑉 ≠ ∅))
7	6	biimpa 501	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) ≠ 0) → 𝑉 ≠ ∅)
8		elnnne0 11306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝑉) ∈ ℕ ↔ ((#‘𝑉) ∈ ℕ₀ ∧ (#‘𝑉) ≠ 0))
9		df-ne 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((#‘𝑉) ≠ 1 ↔ ¬ (#‘𝑉) = 1)
10		eluz2b3 11762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑉) ∈ (ℤ_≥‘2) ↔ ((#‘𝑉) ∈ ℕ ∧ (#‘𝑉) ≠ 1))
11		hash2prde 13252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 2) → ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))
12		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑎 ∈ V
13	12	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑎 ≠ 𝑏 → 𝑎 ∈ V)
14		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑏 ∈ V
15	14	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑎 ≠ 𝑏 → 𝑏 ∈ V)
16		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑎 ≠ 𝑏 → 𝑎 ≠ 𝑏)
17	13, 15, 16	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑎 ≠ 𝑏 → (𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏))
18		frgrreggt1.v	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑉 = (Vtx‘𝐺)
19	18	eqeq1i 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑉 = {𝑎, 𝑏} ↔ (Vtx‘𝐺) = {𝑎, 𝑏})
20	19	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑉 = {𝑎, 𝑏} → (Vtx‘𝐺) = {𝑎, 𝑏})
21		nfrgr2v 27136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑎 ≠ 𝑏) ∧ (Vtx‘𝐺) = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph )
22	17, 20, 21	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}) → 𝐺 ∉ FriendGraph )
23		df-nel 2898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1256	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (VtxDeg‘𝐺) = (VtxDeg‘𝐺)
36	18, 35	rusgrprop0 26463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾))
37		eluz2gt1 11760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((#‘𝑉) ∈ (ℤ_≥‘2) → 1 < (#‘𝑉))
38	37	anim2i 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝐺 ∈ FriendGraph ∧ (#‘𝑉) ∈ (ℤ_≥‘2)) → (𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)))
39	38	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (((#‘𝑉) ∈ (ℤ_≥‘2) ∧ 𝐺 ∈ FriendGraph ) → (𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)))
40	18	vdgn0frgrv2 27159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉) → (1 < (#‘𝑉) → ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
41	40	impancom 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)) → (𝑣 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
42	41	ralrimiv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (#‘𝑉)) → ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
43		eqeq2 2633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝐾 = 0 → (((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0))
44	43	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (𝐾 = 0 → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0))
45		r19.26 3064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 0))
46		nne 2798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 ⊢ (¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0 ↔ ((VtxDeg‘𝐺)‘𝑣) = 0)
47	46	bicomi 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (((VtxDeg‘𝐺)‘𝑣) = 0 ↔ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0)
48	47	anbi1i 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)
51	50	bifal 1497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((((VtxDeg‘𝐺)‘𝑣) ≠ 0 ∧ ¬ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥)
52	48, 49, 51	3bitri 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ⊥)
53	52	ralbii 2980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 0 ∧ ((VtxDeg‘𝐺)‘𝑣) ≠ 0) ↔ ∀𝑣 ∈ 𝑉 ⊥)
54		r19.3rzv 4064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (𝑉 ≠ ∅ → (⊥ ↔ ∀𝑣 ∈ 𝑉 ⊥))
55		falim 1498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 27205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))
75	74	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾)) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))
76		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝐾 = 2 → 𝐾 = 2)
77		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝐾 = 2 → (𝐾 − 1) = (2 − 1))
78	76, 77	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝐾 = 2 → (𝐾 · (𝐾 − 1)) = (2 · (2 − 1)))
79	78	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = ((2 · (2 − 1)) + 1))
80		2m1e1 11135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (2 − 1) = 1
81	80	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (2 · (2 − 1)) = (2 · 1)
82		2t1e2 11176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (2 · 1) = 2
83	81, 82	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (2 · (2 − 1)) = 2
84	83	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((2 · (2 − 1)) + 1) = (2 + 1)
85		2p1e3 11151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (2 + 1) = 3
86	84, 85	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((2 · (2 − 1)) + 1) = 3
87	79, 86	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐾 = 2 → ((𝐾 · (𝐾 − 1)) + 1) = 3)
88	87	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐾 = 2 → ((#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1) ↔ (#‘𝑉) = 3))
89		pm2.21 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (¬ (#‘𝑉) = 3 → ((#‘𝑉) = 3 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))
90	89	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 27252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1256	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . . . . . . . . . . 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 1256	. . . . . . . . . 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 1256	. . . . . 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 1283	. . 3 ⊢ ((#‘𝑉) ∈ ℕ₀ → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3)))))
132	1, 131	mpcom 38	. 2 ⊢ (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → (𝐺 RegUSGraph 𝐾 → ((#‘𝑉) = 0 ∨ (#‘𝑉) = 1 ∨ (#‘𝑉) = 3))))
133	132	3imp21 1277	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 1483 ⊥wfal 1488 ∃wex 1704 ∈ wcel 1990 ≠ wne 2794 ∉ wnel 2897 ∀wral 2912 Vcvv 3200 ∅c0 3915 {cpr 4179 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 − cmin 10266 ℕcn 11020 2c2 11070 3c3 11071 ℕ₀cn0 11292 ℕ₀^*cxnn0 11363 ℤ_≥cuz 11687 #chash 13117 Vtxcvtx 25874 USGraph cusgr 26044 VtxDegcvtxdg 26361 RegUSGraph crusgr 26452 FriendGraph cfrgr 27120

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-ac2 9285 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

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 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-ec 7744 df-qs 7748 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-ac 8939 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-rp 11833 df-xadd 11947 df-ico 12181 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-word 13299 df-lsw 13300 df-concat 13301 df-s1 13302 df-substr 13303 df-reps 13306 df-csh 13535 df-s2 13593 df-s3 13594 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-dvds 14984 df-gcd 15217 df-prm 15386 df-phi 15471 df-vtx 25876 df-iedg 25877 df-edg 25940 df-uhgr 25953 df-ushgr 25954 df-upgr 25977 df-umgr 25978 df-uspgr 26045 df-usgr 26046 df-fusgr 26209 df-nbgr 26228 df-vtxdg 26362 df-rgr 26453 df-rusgr 26454 df-wlks 26495 df-wlkson 26496 df-trls 26589 df-trlson 26590 df-pths 26612 df-spths 26613 df-pthson 26614 df-spthson 26615 df-wwlks 26722 df-wwlksn 26723 df-wwlksnon 26724 df-wspthsn 26725 df-wspthsnon 26726 df-clwwlks 26877 df-clwwlksn 26878 df-conngr 27047 df-frgr 27121

This theorem is referenced by: frgrregord13 27254

W3C validator