Definition df-ofs 36196

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 29023). See brofs 36218 and 5segofs 36219 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.)

Assertion

Ref	Expression
df-ofs	⊢ OuterFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}

Distinct variable group:   𝑎,𝑏,𝑐,𝑑,𝑥,𝑦,𝑧,𝑤,𝑝,𝑞,𝑛

Detailed syntax breakdown of Definition df-ofs

Step	Hyp	Ref	Expression
1		cofs 36195	. 2 class OuterFiveSeg
2		vp	. . . . . . . . . . . . . . 15 setvar 𝑝
3	2	cv 1541	. . . . . . . . . . . . . 14 class 𝑝
4		va	. . . . . . . . . . . . . . . . 17 setvar 𝑎
5	4	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑎
6		vb	. . . . . . . . . . . . . . . . 17 setvar 𝑏
7	6	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑏
8	5, 7	cop 4588	. . . . . . . . . . . . . . 15 class ⟨𝑎, 𝑏⟩
9		vc	. . . . . . . . . . . . . . . . 17 setvar 𝑐
10	9	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑐
11		vd	. . . . . . . . . . . . . . . . 17 setvar 𝑑
12	11	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑑
13	10, 12	cop 4588	. . . . . . . . . . . . . . 15 class ⟨𝑐, 𝑑⟩
14	8, 13	cop 4588	. . . . . . . . . . . . . 14 class ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
15	3, 14	wceq 1542	. . . . . . . . . . . . 13 wff 𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
16		vq	. . . . . . . . . . . . . . 15 setvar 𝑞
17	16	cv 1541	. . . . . . . . . . . . . 14 class 𝑞
18		vx	. . . . . . . . . . . . . . . . 17 setvar 𝑥
19	18	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑥
20		vy	. . . . . . . . . . . . . . . . 17 setvar 𝑦
21	20	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑦
22	19, 21	cop 4588	. . . . . . . . . . . . . . 15 class ⟨𝑥, 𝑦⟩
23		vz	. . . . . . . . . . . . . . . . 17 setvar 𝑧
24	23	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑧
25		vw	. . . . . . . . . . . . . . . . 17 setvar 𝑤
26	25	cv 1541	. . . . . . . . . . . . . . . 16 class 𝑤
27	24, 26	cop 4588	. . . . . . . . . . . . . . 15 class ⟨𝑧, 𝑤⟩
28	22, 27	cop 4588	. . . . . . . . . . . . . 14 class ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
29	17, 28	wceq 1542	. . . . . . . . . . . . 13 wff 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
30	5, 10	cop 4588	. . . . . . . . . . . . . . . 16 class ⟨𝑎, 𝑐⟩
31		cbtwn 28973	. . . . . . . . . . . . . . . 16 class Btwn
32	7, 30, 31	wbr 5100	. . . . . . . . . . . . . . 15 wff 𝑏 Btwn ⟨𝑎, 𝑐⟩
33	19, 24	cop 4588	. . . . . . . . . . . . . . . 16 class ⟨𝑥, 𝑧⟩
34	21, 33, 31	wbr 5100	. . . . . . . . . . . . . . 15 wff 𝑦 Btwn ⟨𝑥, 𝑧⟩
35	32, 34	wa 395	. . . . . . . . . . . . . 14 wff (𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩)
36		ccgr 28974	. . . . . . . . . . . . . . . 16 class Cgr
37	8, 22, 36	wbr 5100	. . . . . . . . . . . . . . 15 wff ⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩
38	7, 10	cop 4588	. . . . . . . . . . . . . . . 16 class ⟨𝑏, 𝑐⟩
39	21, 24	cop 4588	. . . . . . . . . . . . . . . 16 class ⟨𝑦, 𝑧⟩
40	38, 39, 36	wbr 5100	. . . . . . . . . . . . . . 15 wff ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩
41	37, 40	wa 395	. . . . . . . . . . . . . 14 wff (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩)
42	5, 12	cop 4588	. . . . . . . . . . . . . . . 16 class ⟨𝑎, 𝑑⟩
43	19, 26	cop 4588	. . . . . . . . . . . . . . . 16 class ⟨𝑥, 𝑤⟩
44	42, 43, 36	wbr 5100	. . . . . . . . . . . . . . 15 wff ⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩
45	7, 12	cop 4588	. . . . . . . . . . . . . . . 16 class ⟨𝑏, 𝑑⟩
46	21, 26	cop 4588	. . . . . . . . . . . . . . . 16 class ⟨𝑦, 𝑤⟩
47	45, 46, 36	wbr 5100	. . . . . . . . . . . . . . 15 wff ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩
48	44, 47	wa 395	. . . . . . . . . . . . . 14 wff (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)
49	35, 41, 48	w3a 1087	. . . . . . . . . . . . 13 wff ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))
50	15, 29, 49	w3a 1087	. . . . . . . . . . . 12 wff (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
51		vn	. . . . . . . . . . . . . 14 setvar 𝑛
52	51	cv 1541	. . . . . . . . . . . . 13 class 𝑛
53		cee 28972	. . . . . . . . . . . . 13 class 𝔼
54	52, 53	cfv 6500	. . . . . . . . . . . 12 class (𝔼‘𝑛)
55	50, 25, 54	wrex 3062	. . . . . . . . . . 11 wff ∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
56	55, 23, 54	wrex 3062	. . . . . . . . . 10 wff ∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
57	56, 20, 54	wrex 3062	. . . . . . . . 9 wff ∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
58	57, 18, 54	wrex 3062	. . . . . . . 8 wff ∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
59	58, 11, 54	wrex 3062	. . . . . . 7 wff ∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
60	59, 9, 54	wrex 3062	. . . . . 6 wff ∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
61	60, 6, 54	wrex 3062	. . . . 5 wff ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
62	61, 4, 54	wrex 3062	. . . 4 wff ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
63		cn 12157	. . . 4 class ℕ
64	62, 51, 63	wrex 3062	. . 3 wff ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
65	64, 2, 16	copab 5162	. 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}
66	1, 65	wceq 1542	1 wff OuterFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}

This definition is referenced by:  brofs  36218