Definition df-ofs 35971

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 28865). See brofs 35993 and 5segofs 35994 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 35970	. 2 class OuterFiveSeg
2		vp	. . . . . . . . . . . . . . 15 setvar 𝑝
3	2	cv 1539	. . . . . . . . . . . . . 14 class 𝑝
4		va	. . . . . . . . . . . . . . . . 17 setvar 𝑎
5	4	cv 1539	. . . . . . . . . . . . . . . 16 class 𝑎
6		vb	. . . . . . . . . . . . . . . . 17 setvar 𝑏
7	6	cv 1539	. . . . . . . . . . . . . . . 16 class 𝑏
8	5, 7	cop 4595	. . . . . . . . . . . . . . 15 class ⟨𝑎, 𝑏⟩
9		vc	. . . . . . . . . . . . . . . . 17 setvar 𝑐
10	9	cv 1539	. . . . . . . . . . . . . . . 16 class 𝑐
11		vd	. . . . . . . . . . . . . . . . 17 setvar 𝑑
12	11	cv 1539	. . . . . . . . . . . . . . . 16 class 𝑑
13	10, 12	cop 4595	. . . . . . . . . . . . . . 15 class ⟨𝑐, 𝑑⟩
14	8, 13	cop 4595	. . . . . . . . . . . . . 14 class ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
15	3, 14	wceq 1540	. . . . . . . . . . . . 13 wff 𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
16		vq	. . . . . . . . . . . . . . 15 setvar 𝑞
17	16	cv 1539	. . . . . . . . . . . . . 14 class 𝑞
18		vx	. . . . . . . . . . . . . . . . 17 setvar 𝑥
19	18	cv 1539	. . . . . . . . . . . . . . . 16 class 𝑥
20		vy	. . . . . . . . . . . . . . . . 17 setvar 𝑦
21	20	cv 1539	. . . . . . . . . . . . . . . 16 class 𝑦
22	19, 21	cop 4595	. . . . . . . . . . . . . . 15 class ⟨𝑥, 𝑦⟩
23		vz	. . . . . . . . . . . . . . . . 17 setvar 𝑧
24	23	cv 1539	. . . . . . . . . . . . . . . 16 class 𝑧
25		vw	. . . . . . . . . . . . . . . . 17 setvar 𝑤
26	25	cv 1539	. . . . . . . . . . . . . . . 16 class 𝑤
27	24, 26	cop 4595	. . . . . . . . . . . . . . 15 class ⟨𝑧, 𝑤⟩
28	22, 27	cop 4595	. . . . . . . . . . . . . 14 class ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
29	17, 28	wceq 1540	. . . . . . . . . . . . 13 wff 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
30	5, 10	cop 4595	. . . . . . . . . . . . . . . 16 class ⟨𝑎, 𝑐⟩
31		cbtwn 28816	. . . . . . . . . . . . . . . 16 class Btwn
32	7, 30, 31	wbr 5107	. . . . . . . . . . . . . . 15 wff 𝑏 Btwn ⟨𝑎, 𝑐⟩
33	19, 24	cop 4595	. . . . . . . . . . . . . . . 16 class ⟨𝑥, 𝑧⟩
34	21, 33, 31	wbr 5107	. . . . . . . . . . . . . . 15 wff 𝑦 Btwn ⟨𝑥, 𝑧⟩
35	32, 34	wa 395	. . . . . . . . . . . . . 14 wff (𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩)
36		ccgr 28817	. . . . . . . . . . . . . . . 16 class Cgr
37	8, 22, 36	wbr 5107	. . . . . . . . . . . . . . 15 wff ⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩
38	7, 10	cop 4595	. . . . . . . . . . . . . . . 16 class ⟨𝑏, 𝑐⟩
39	21, 24	cop 4595	. . . . . . . . . . . . . . . 16 class ⟨𝑦, 𝑧⟩
40	38, 39, 36	wbr 5107	. . . . . . . . . . . . . . 15 wff ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩
41	37, 40	wa 395	. . . . . . . . . . . . . 14 wff (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩)
42	5, 12	cop 4595	. . . . . . . . . . . . . . . 16 class ⟨𝑎, 𝑑⟩
43	19, 26	cop 4595	. . . . . . . . . . . . . . . 16 class ⟨𝑥, 𝑤⟩
44	42, 43, 36	wbr 5107	. . . . . . . . . . . . . . 15 wff ⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩
45	7, 12	cop 4595	. . . . . . . . . . . . . . . 16 class ⟨𝑏, 𝑑⟩
46	21, 26	cop 4595	. . . . . . . . . . . . . . . 16 class ⟨𝑦, 𝑤⟩
47	45, 46, 36	wbr 5107	. . . . . . . . . . . . . . 15 wff ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩
48	44, 47	wa 395	. . . . . . . . . . . . . 14 wff (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)
49	35, 41, 48	w3a 1086	. . . . . . . . . . . . 13 wff ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))
50	15, 29, 49	w3a 1086	. . . . . . . . . . . 12 wff (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
51		vn	. . . . . . . . . . . . . 14 setvar 𝑛
52	51	cv 1539	. . . . . . . . . . . . 13 class 𝑛
53		cee 28815	. . . . . . . . . . . . 13 class 𝔼
54	52, 53	cfv 6511	. . . . . . . . . . . 12 class (𝔼‘𝑛)
55	50, 25, 54	wrex 3053	. . . . . . . . . . 11 wff ∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
56	55, 23, 54	wrex 3053	. . . . . . . . . 10 wff ∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
57	56, 20, 54	wrex 3053	. . . . . . . . 9 wff ∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
58	57, 18, 54	wrex 3053	. . . . . . . 8 wff ∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
59	58, 11, 54	wrex 3053	. . . . . . 7 wff ∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
60	59, 9, 54	wrex 3053	. . . . . 6 wff ∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
61	60, 6, 54	wrex 3053	. . . . 5 wff ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
62	61, 4, 54	wrex 3053	. . . 4 wff ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
63		cn 12186	. . . 4 class ℕ
64	62, 51, 63	wrex 3053	. . 3 wff ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
65	64, 2, 16	copab 5169	. 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}
66	1, 65	wceq 1540	1 wff OuterFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}

This definition is referenced by:  brofs  35993